> module rat_times where;

> import rat_plus;

> [timesQ [q, r : PreQ] = (div (timesZ (pi1 ? ? q) (pi1 ? ? r)) (timesZ (pi2 ? ? q) (pi2 ? ? r)))];

> Claim timesQtotal : (q, r : PreQ) Rational q -> Rational r -> Rational (timesQ q r);
> Intros q r;
> Refine timesZ_not_zero;
> ReturnAll;
> timesQtotal;

> [timesQwdl : (q, q', r : PreQ) EqQ q q' -> EqQ (timesQ q r) (timesQ q' r)];
> [timesQwdr : (q, r, r' : PreQ) EqQ r r' -> EqQ (timesQ q r) (timesQ q r')];

> Claim timesQwd : (q, q', r, r' : PreQ) Rational q' -> Rational r -> EqQ q q' -> EqQ r r' -> EqQ (timesQ q r) (timesQ q' r');
> Intros q q' r r' ratq' ratr q_is_q' r_is_r';
> Refine EqQ_trans ? (timesQ q' r);
> Refine timesQwdr;
> Refine r_is_r';
> Refine timesQwdl;
> Refine q_is_q';
> Refine timesQtotal;
> Refine ratr;
> Refine ratq';
> ReturnAll;

> Claim ZtoQtimes : (x, y : Int) EqQ (timesZ x y) (timesQ x y);
> Intros x y;
> Refine EqQ_ref;
> ReturnAll;
> ZtoQtimes;

> Claim timesQ_comm : (q, r : PreQ) EqQ (timesQ q r) (timesQ r q);
> Intros q r;
> [a = pi1 ? ? q];
> [b = pi2 ? ? q];
> [c = pi1 ? ? r];
> [d = pi2 ? ? r];
> Refine timesZwd (timesZ a c) (timesZ c a) (timesZ d b) (timesZ b d);
> Refine timesZ_comm;
> Refine timesZ_comm;
> ReturnAll;
> timesQ_comm;

> Claim timesQ_assocl : (q, r, s : PreQ) EqQ (timesQ q (timesQ r s)) (timesQ (timesQ q r) s);
> Intros q r s;
> [a = pi1 ? ? q];
> [b = pi2 ? ? q];
> [c = pi1 ? ? r];
> [d = pi2 ? ? r];
> [e = pi1 ? ? s];
> [f = pi2 ? ? s];
> Refine timesZwd (timesZ a (timesZ c e)) (timesZ (timesZ a c) e) (timesZ (timesZ b d) f) (timesZ b (timesZ d f));
> Refine timesZ_assocr;
> Refine timesZ_assocl;
> ReturnAll;
> timesQ_assocl;

> Claim timesQ_assocr : (q, r, s : PreQ) EqQ (timesQ (timesQ q r) s) (timesQ q (timesQ r s));
> Intros q r s;
> Refine EqQ_sym;
> Refine timesQ_assocl;
> ReturnAll;
> timesQ_assocr;

> Claim timesQ_plusQ_distl : (q, r, s : PreQ) EqQ (timesQ q (plusQ r s)) (plusQ (timesQ q r) (timesQ q s));
> Intros q r s;
> [a = pi1 ? ? q];
> [b = pi2 ? ? q];
> [c = pi1 ? ? r];
> [d = pi2 ? ? r];
> [e = pi1 ? ? s];
> [f = pi2 ? ? s];
> Refine EqZ_trans (timesZ (timesZ a (plusZ (timesZ c f) (timesZ e d))) (timesZ (timesZ b d) (timesZ b f)))
>                  (timesZ (timesZ a (plusZ (timesZ c f) (timesZ e d))) (timesZ b (timesZ b (timesZ d f))))
>                  (timesZ (plusZ (timesZ (timesZ a c) (timesZ b f)) (timesZ (timesZ a e) (timesZ b d))) (timesZ b (timesZ d f)));
> 2 Refine timesZwdr (timesZ a (plusZ (timesZ c f) (timesZ e d))) (timesZ (timesZ b d) (timesZ b f)) (timesZ b (timesZ b (timesZ d f)));
> 2 Refine EqZ_trans ? (timesZ b (timesZ d (timesZ b f)));
> 3 Refine timesZ_assocr b d (timesZ b f);
> 2 Refine timesZwdr b (timesZ d (timesZ b f)) (timesZ b (timesZ d f));
> 2 Refine EqZ_trans ? (timesZ (timesZ d b) f);
> 3 Refine timesZ_assocl;
> 2 Refine EqZ_trans ? (timesZ (timesZ b d) f);
> 3 Refine timesZwdl (timesZ d b) (timesZ b d) f;
> 3 Refine timesZ_comm;
> 2 Refine timesZ_assocr;
> Refine EqZ_trans ? (timesZ (timesZ (timesZ a (plusZ (timesZ c f) (timesZ e d))) b) (timesZ b (timesZ d f)));
> 2 Refine timesZ_assocl (timesZ a (plusZ (timesZ c f) (timesZ e d))) b (timesZ b (timesZ d f));
> Refine timesZwdl (timesZ (timesZ a (plusZ (timesZ c f) (timesZ e d))) b) (plusZ (timesZ (timesZ a c) (timesZ b f)) (timesZ (timesZ a e) (timesZ b d))) (timesZ b (timesZ d f));
> Refine EqZ_trans ? (timesZ (plusZ (timesZ a (timesZ c f)) (timesZ a (timesZ e d))) b);
> 2 Refine timesZwdl (timesZ a (plusZ (timesZ c f) (timesZ e d))) (plusZ (timesZ a (timesZ c f)) (timesZ a (timesZ e d))) b;
> 2 Refine timesZ_plusZ_distl a (timesZ c f) (timesZ e d);
> Refine EqZ_trans ? (plusZ (timesZ (timesZ a (timesZ c f)) b) (timesZ (timesZ a (timesZ e d)) b));
> 2 Refine timesZ_plusZ_distr (timesZ a (timesZ c f)) (timesZ a (timesZ e d)) b;
> Refine plusZwd (timesZ (timesZ a (timesZ c f)) b) (timesZ (timesZ a c) (timesZ b f)) (timesZ (timesZ a (timesZ e d)) b) (timesZ (timesZ a e) (timesZ b d));
> 2 Refine EqZ_trans ? (timesZ (timesZ (timesZ a c) f) b);
> 3 Refine timesZwdl (timesZ a (timesZ c f)) (timesZ (timesZ a c) f) b;
> 3 Refine timesZ_assocl;
> 2 Refine EqZ_trans ? (timesZ (timesZ a c) (timesZ f b));
> 3 Refine timesZ_assocr (timesZ a c);
> 2 Refine timesZwdr (timesZ a c) (timesZ f b) (timesZ b f);
> 2 Refine timesZ_comm;
> Refine EqZ_trans ? (timesZ (timesZ (timesZ a e) d) b);
> 2 Refine timesZwdl (timesZ a (timesZ e d)) (timesZ (timesZ a e) d);
> 2 Refine timesZ_assocl;
> Refine EqZ_trans ? (timesZ (timesZ a e) (timesZ d b));
> 2 Refine timesZ_assocr (timesZ a e);
> Refine timesZwdr (timesZ a e) (timesZ d b) (timesZ b d);
> Refine timesZ_comm;
> ReturnAll;
> timesQ_plusQ_distl;

> Claim timesQ_plusQ_distr : (q, r, s : PreQ) Rational q -> Rational r -> Rational s ->
>   EqQ (timesQ (plusQ q r) s) (plusQ (timesQ q s) (timesQ r s));
> Intros q r s ratq ratr rats;
> Refine EqQ_trans ? (timesQ s (plusQ q r));
> 3 Refine timesQtotal s (plusQ q r);
> 4 Refine rats;
> 3 Refine plusQtotal;
> 4 Refine ratq;
> 3 Refine ratr;
> 2 Refine timesQ_comm (plusQ q r);
> Refine EqQ_trans ? (plusQ (timesQ s q) (timesQ s r));
> 3 Refine plusQtotal (timesQ s q) (timesQ s r);
> 4 Refine timesQtotal;
> 5 Refine rats;
> 4 Refine ratq;
> 3 Refine timesQtotal;
> 4 Refine rats;
> 3 Refine ratr;
> 2 Refine timesQ_plusQ_distl;
> Refine plusQwd (timesQ s q) (timesQ q s) (timesQ s r) (timesQ r s);
> 2 Refine timesQ_comm;
> Refine timesQ_comm;
> ReturnAll;
> timesQ_plusQ_distr;

> Claim timesQ_one : (q : PreQ) EqQ (timesQ q one) q;
> Intros q;
> [a = pi1 ? ? q];
> [b = pi2 ? ? q];
> Refine timesZwd (timesZ a one) a b (timesZ b one);
> Refine EqZ_sym;
> Refine timesZ_one;
> Refine timesZ_one;
> ReturnAll;
> timesQ_one;

> Claim zero_timesQ : (q : PreQ) EqQ (timesQ zero q) zero;
> Intros q;
> [a = pi1 ? ? q];
> [b = pi2 ? ? q];
> Refine EqZ_trans (timesZ (timesZ zero a) one) (timesZ zero a) (timesZ zero (timesZ one b));
> 2 Refine timesZ_one;
> Refine EqZ_trans ? zero;
> 2 Refine zero_timesZ;
> Refine EqZ_sym;
> Refine zero_timesZ (timesZ one b);
> ReturnAll;
> zero_timesQ;

> [invQ [q : PreQ] = div (pi2 ? ? q) (pi1 ? ? q)];

> Claim invQwd : (q, q' : PreQ) EqQ q q' -> EqQ (invQ q) (invQ q');
> Intros q q' q_is_q';
> [a = pi1 ? ? q];
> [b = pi2 ? ? q];
> [a' = pi1 ? ? q'];
> [b' = pi2 ? ? q'];
> Refine EqZ_trans (timesZ b a') (timesZ a' b) (timesZ b' a);
> 2 Refine timesZ_comm;
> Refine EqZ_trans ? (timesZ a b');
> 2 Refine EqZ_sym;
> 2 Refine q_is_q';
> Refine timesZ_comm;
> ReturnAll;
> invQwd;

> Claim invQtotal : (q : PreQ) Not (EqQ q zero) -> Rational (invQ q);
> Intros q q_not_zero;
> [a = pi1 ? ? q];
> [b = pi2 ? ? q];
> Refine NotI (EqZ a zero);
> Intros a_is_zero;
> [a = pi1 ? ? q];
> [b = pi2 ? ? q];
> Refine NotE (EqZ (timesZ a one) (timesZ zero b));
> 2 Refine q_not_zero;
> Refine EqZ_trans ? a;
> 2 Refine timesZ_one;
> Refine EqZ_trans ? zero;
> 2 Refine a_is_zero;
> Refine EqZ_sym;
> Refine zero_timesZ;
> ReturnAll;
> invQtotal;

> Claim timesQ_invQ : (q : PreQ) EqQ (timesQ q (invQ q)) one;
> Intros q;
> [a = pi1 ? ? q];
> [b = pi2 ? ? q];
> Refine EqZ_trans (timesZ (timesZ a b) one) (timesZ a b) (timesZ one (timesZ b a));
> 2 Refine timesZ_one;
> Refine EqZ_trans ? (timesZ b a);
> 2 Refine timesZ_comm;
> Refine EqZ_sym;
> Refine one_timesZ (timesZ b a);
> ReturnAll;
> timesQ_invQ;

> [halfplushalf : (q : PreQ) Rational q -> EqQ (plusQ (timesQ q (invQ two)) (timesQ q (invQ two))) q];
> [two_halves : (q : PreQ) Rational q -> EqQ (timesQ (plusQ q q) (invQ two)) q];