> module int_times where;

> import nat_times;
> import int_plus;

Multiplication

> [timesZ [x, y : Int] = minus (plus (times (pi1 ? ? x) (pi1 ? ? y)) (times (pi2 ? ? x) (pi2 ? ? y)))
>   (plus (times (pi1 ? ? x) (pi2 ? ? y)) (times (pi2 ? ? x) (pi1 ? ? y)))];

> Claim timesZwdl : (x, x', y : Int) EqZ x x' -> EqZ (timesZ x y) (timesZ x' y);
> Intros x x' y x_is_x';
> [a = pi1 ? ? x];
> [b = pi2 ? ? x];
> [a' = pi1 ? ? x'];
> [b' = pi2 ? ? x'];
> [c = pi1 ? ? y];
> [d = pi2 ? ? y];
> Refine trans nat (plus (plus (times a c) (times b d)) (plus (times a' d) (times b' c))) 
>                (plus (plus (times a c) (times b' c)) (plus (times a' d) (times b d)))
>                (plus (plus (times a' c) (times b' d)) (plus (times a d) (times b c)));
> Refine trans nat ? (plus (plus (times a' c) (times b c)) (plus (times a d) (times b' d)));
> Refine trans nat ? (plus (times a' c) (plus (times b c) (plus (times a d) (times b' d))));
> Refine trans nat ? (plus (times a' c) (plus (times b' d) (plus (times a d) (times b c))));
> Refine plus_assocl;
> Refine wd nat nat (plus (times a' c));
> Refine trans nat ? (plus (plus (times b c) (times a d)) (times b' d));
> Refine trans nat ? (plus (times b' d) (plus (times b c) (times a d)));
> Refine wd nat nat (plus (times b' d));
> Refine plus_comm;
> Refine plus_comm;
> Refine plus_assocl;
> Refine plus_assocr;
> Refine wd2 nat nat nat plus;
> Refine trans nat ? (times (plus a' b) d);
> Refine trans nat ? (times (plus a b') d);
> Refine times_plus_distr;
> Refine wd nat nat [z : Nat] times z d;
> Refine sym;
> Refine x_is_x';
> Refine times_plus_distr';
> Refine trans nat ? (times (plus a b') c);
> Refine trans nat ? (times (plus a' b) c);
> Refine times_plus_distr;
> Refine wd nat nat [z : Nat] times z c;
> Refine x_is_x';
> Refine times_plus_distr';
> Refine trans nat ? (plus (times a c) (plus (times b d) (plus (times a' d) (times b' c))));
> Refine trans nat ? (plus (times a c) (plus (times b' c) (plus (times a' d) (times b d))));
> Refine plus_assocl;
> Refine wd nat nat (plus (times a c));
> Refine trans nat ? (plus (plus (times b d) (times a' d)) (times b' c));
> Refine trans nat ? (plus (times b' c) (plus (times b d) (times a' d)));
> Refine wd nat nat (plus (times b' c));
> Refine plus_comm;
> Refine plus_comm;
> Refine plus_assocl;
> Refine plus_assocr;
> ReturnAll;
> timesZwdl;

> Claim timesZ_comm : (x, y : Int) EqZ (timesZ x y) (timesZ y x);
> Intros x y;
> [a = pi1 ? ? x];
> [b = pi2 ? ? x];
> [c = pi1 ? ? y];
> [d = pi2 ? ? y];
> Refine wd2 nat nat nat plus;
> 2 Refine wd2 nat nat nat plus;
> 3 Refine times_comm;
> 2 Refine times_comm;
> Refine trans nat (plus (times c b) (times d a)) (plus (times d a) (times c b)) (plus (times a d) (times b c));
> 2 Refine plus_comm;
> Refine wd2 nat nat nat plus;
> 2 Refine times_comm;
> Refine times_comm;
> ReturnAll;
> timesZ_comm;

> Claim timesZwdr : (x, y, y' : Int) EqZ y y' -> EqZ (timesZ x y) (timesZ x y');
> Intros x y y' y_is_y';
> Refine EqZ_trans ? (timesZ y x);
> Refine EqZ_trans ? (timesZ y' x);
> Refine timesZ_comm;
> Refine timesZwdl;
> Refine y_is_y';
> Refine timesZ_comm;
> ReturnAll;

> Claim timesZwd : (x, x', y, y' : Int) EqZ x x' -> EqZ y y' -> EqZ (timesZ x y) (timesZ x' y');
> Intros x x' y y' x_is_x' y_is_y';
> Refine EqZ_trans ? (timesZ x' y);
> Refine timesZwdr;
> Refine y_is_y';
> Refine timesZwdl;
> Refine x_is_x';
> ReturnAll;
> timesZwd;

> Claim NtoZtimes : (m, n : Nat) EqZ (times m n) (timesZ m n);
> Intros m n;
> Refine wd2 nat nat nat plus;
> Refine trans nat ? (times zero n);
> Refine zero_times;
> Refine zero_plus;
> Refine EqI;
> ReturnAll;
> NtoZtimes;

> Claim timesZ_assocl : (x, y, z : Int) EqZ (timesZ x (timesZ y z)) (timesZ (timesZ x y) z);
> Intros x y z;
> [a = pi1 ? ? x];
> [b = pi2 ? ? x];
> [c = pi1 ? ? y];
> [d = pi2 ? ? y];
> [e = pi1 ? ? z];
> [f = pi2 ? ? z];
> Refine wd2 nat nat nat plus;
> 2 Refine trans nat ? (plus (plus (times a (times c e)) (times a (times d f))) (plus (times b (times c f)) (times b (times d e))));
> 3 Refine wd2 nat nat nat plus;
> 4 Refine times_plus_distl;
> 3 Refine times_plus_distl;
> 2 Refine trans nat ? (plus (plus (times (times a c) e) (times (times a d) f)) (plus (times (times b c) f) (times (times b d) e)));
> 3 Refine wd2 nat nat nat plus;
> 4 Refine wd2 nat nat nat plus;
> 5 Refine times_assocl;
> 4 Refine times_assocl;
> 3 Refine wd2 nat nat nat plus;
> 4 Refine times_assocl;
> 3 Refine times_assocl;
> 2 Refine trans nat ? (plus (times (times a c) e) (plus (times (times a d) f) (plus (times (times b c) f) (times (times b d) e))));
> 3 Refine plus_assocr;
> 2 Refine trans nat ? (plus (times (times a c) e) (plus (times (times b d) e) (times (plus (times a d) (times b c)) f)));
> 3 Refine wd nat nat (plus (times (times a c) e));
> 3 Refine trans nat ? (plus (plus (times (times a d) f) (times (times b c) f)) (times (times b d) e));
> 4 Refine plus_assocl;
> 3 Refine trans nat ? (plus (times (times b d) e) (plus (times (times a d) f) (times (times b c) f)));
> 4 Refine plus_comm;
> 3 Refine wd nat nat (plus (times (times b d) e));
> 3 Refine times_plus_distr';
> 2 Refine trans nat ? (plus (plus (times (times a c) e) (times (times b d) e)) (times (plus (times a d) (times b c)) f));
> 3 Refine plus_assocl;
> 2 Refine wd nat nat [t : Nat] plus t (times (plus (times a d) (times b c)) f);
> 2 Refine times_plus_distr';
> Refine trans nat ? (plus (plus (times a (times c f)) (times b (times d f))) (plus (times a (times d e)) (times b (times c e))));
> 2 Refine wd2 nat nat nat plus;
> 3 Refine trans nat ? (plus (times (times a c) f) (times (times b d) f));
> 4 Refine times_plus_distr;
> 3 Refine wd2 nat nat nat plus;
> 4 Refine times_assocr;
> 3 Refine times_assocr;
> 2 Refine trans nat ? (plus (times (times a d) e) (times (times b c) e));
> 3 Refine times_plus_distr;
> 2 Refine wd2 nat nat nat plus;
> 3 Refine times_assocr;
> 2 Refine times_assocr;
> Refine trans nat ? (plus (times a (times c f)) (plus (times b (times d f)) (plus (times a (times d e)) (times b (times c e)))));
> 2 Refine plus_assocr;
> Refine trans nat ? (plus (times a (times c f)) (plus (times a (times d e)) (times b (plus (times c e) (times d f)))));
> 2 Refine wd nat nat (plus (times a (times c f)));
> 2 Refine trans nat ? (plus (plus (times a (times d e)) (times b (times c e))) (times b (times d f)));
> 3 Refine plus_comm;
> 2 Refine trans nat ? (plus (times a (times d e)) (plus (times b (times c e)) (times b (times d f))));
> 3 Refine plus_assocr;
> 2 Refine wd nat nat (plus (times a (times d e)));
> 2 Refine times_plus_distl';
> Refine trans nat ? (plus (plus (times a (times c f)) (times a (times d e))) (times b (plus (times c e) (times d f))));
> 2 Refine plus_assocl;
> Refine wd nat nat [t : Nat] plus t (times b (plus (times c e) (times d f)));
> Refine times_plus_distl';
> ReturnAll;

> Claim timesZ_assocr : (x, y, z : Int) EqZ (timesZ (timesZ x y) z) (timesZ x (timesZ y z));
> Intros x y z;
> Refine EqZ_sym (timesZ x (timesZ y z));
> Refine timesZ_assocl;
> ReturnAll;

> Claim timesZ_zero : (x : Int) EqZ (timesZ x zero) zero;
> Intros x;
> Refine EqI;
> ReturnAll;
> timesZ_zero;

> Claim zero_timesZ : (x : Int) EqZ (timesZ zero x) zero;
> Intros x;
> Refine timesZ_comm zero x;
> ReturnAll;
> zero_timesZ;

> Claim timesZ_one : (x : Int) EqZ (timesZ x one) x;
> Intros x;
> [a = pi1 ? ? x];
> [b = pi2 ? ? x];
> Refine wd2 nat nat nat plus;
> 2 Refine zero_plus;
> Refine sym;
> Refine trans nat (plus zero (plus zero b)) (plus zero b) b;
> 2 Refine zero_plus;
> Refine zero_plus;
> ReturnAll;
> timesZ_one;

> Claim one_timesZ : (x : Int) EqZ (timesZ one x) x;
> Intros x;
> Refine EqZ_trans ? (timesZ x one);
> 2 Refine timesZ_comm one;
> Refine timesZ_one;
> ReturnAll;
> one_timesZ;

> Claim timesZ_plusZ_distr : (x, y, z : Int) EqZ (timesZ (plusZ x y) z) (plusZ (timesZ x z) (timesZ y z));
> Intros x y z;
> [a = pi1 ? ? x];
> [b = pi2 ? ? x];
> [c = pi1 ? ? y];
> [d = pi2 ? ? y];
> [e = pi1 ? ? z];
> [f = pi2 ? ? z];
> Refine wd2 nat nat nat plus;
> 2 Refine trans nat ? (plus (plus (times a e) (times c e)) (plus (times b f) (times d f)));
> 3 Refine wd2 nat nat nat plus;
> 4 Refine times_plus_distr;
> 3 Refine times_plus_distr;
> 2 Refine trans nat ? (plus (times a e) (plus (times c e) (plus (times b f) (times d f))));
> 3 Refine plus_assocr;
> 2 Refine trans nat ? (plus (times a e) (plus (times b f) (plus (times c e) (times d f))));
> 3 Refine wd nat nat (plus (times a e));
> 3 Refine trans nat ? (plus (plus (times c e) (times b f)) (times d f));
> 4 Refine plus_assocl;
> 3 Refine trans nat ? (plus (plus (times b f) (times c e)) (times d f));
> 4 Refine wd nat nat [z : Nat] plus z (times d f);
> 4 Refine plus_comm;
> 3 Refine plus_assocr;
> 2 Refine plus_assocl;
> Refine trans nat ? (plus (plus (times a f) (times c f)) (plus (times b e) (times d e)));
> 2 Refine trans nat ? (plus (times a f) (plus (times b e) (plus (times c f) (times d e))));
> 3 Refine plus_assocr;
> 2 Refine trans nat ? (plus (times a f) (plus (times c f) (plus (times b e) (times d e))));
> 3 Refine wd nat nat (plus (times a f));
> 3 Refine trans nat ? (plus (plus (times b e) (times c f)) (times d e));
> 4 Refine plus_assocl;
> 3 Refine trans nat ? (plus (plus (times c f) (times b e)) (times d e));
> 4 Refine wd nat nat [z : Nat] plus z (times d e);
> 4 Refine plus_comm;
> 3 Refine plus_assocr;
> 2 Refine plus_assocl;
> Refine wd2 nat nat nat plus;
> 2 Refine times_plus_distr';
> Refine times_plus_distr';
> ReturnAll;

> Claim timesZ_plusZ_distl : (x, y, z : Int) EqZ (timesZ x (plusZ y z)) (plusZ (timesZ x y) (timesZ x z));
> Intros x y z;
> Refine EqZ_trans ? (timesZ (plusZ y z) x);
> 2 Refine timesZ_comm x (plusZ y z);
> Refine EqZ_trans;
> 2 Refine timesZ_plusZ_distr;
> Refine plusZwd (timesZ y x) (timesZ x y) (timesZ z x) (timesZ x z);
> Refine timesZ_comm;
> Refine timesZ_comm;
> ReturnAll;
> timesZ_plusZ_distl;

> Claim timesZ_plusZ_distr' : (x, y, z : Int) EqZ (plusZ (timesZ x z) (timesZ y z)) (timesZ (plusZ x y) z);
> Intros x y z;
> Refine EqZ_sym;
> Refine timesZ_plusZ_distr;
> ReturnAll;
> timesZ_plusZ_distr';

> Claim timesZ_plusZ_distl' : (x, y, z : Int) EqZ (plusZ (timesZ x y) (timesZ x z)) (timesZ x (plusZ y z));
> Intros x y z;
> Refine EqZ_sym;
> Refine timesZ_plusZ_distl;
> ReturnAll;
> timesZ_plusZ_distl';

> Claim timesZ_minusZ : (x, y : Int) EqZ (timesZ x (minusZ y)) (minusZ (timesZ x y));
> Intros x y;
> Refine EqZ_ref;
> ReturnAll;
> timesZ_minusZ;

> Claim minusZ_timesZ : (x, y : Int) EqZ (timesZ (minusZ x) y) (minusZ (timesZ x y));
> Intros x y;
> Refine EqZ_trans ? (timesZ y (minusZ x));
> 2 Refine timesZ_comm (minusZ x);
> Refine EqZ_trans ? (minusZ (timesZ y x));
> 2 Refine timesZ_minusZ;
> Refine minusZwd (timesZ y x) (timesZ x y);
> Refine timesZ_comm;
> ReturnAll;
> minusZ_timesZ;

> Claim timesZ_4lm : (a,b,c,d:Int) EqZ (timesZ (timesZ a b) (timesZ c d)) (timesZ (timesZ a c) (timesZ b d));
> Intros a b c d;
> Refine total_four_lemma Int EqZ timesZ;
> Refine timesZ_comm;
> Refine timesZ_assocl;
> Refine timesZwd;
> Refine EqZ_trans;
> Refine EqZ_sym;
> Refine EqZ_ref;
> ReturnAll;