-change with \forall x,y,z:Z.eq Z (Ztimes (Ztimes x y) z) (Ztimes x (Ztimes y z)).
-intros.
-elim x.simplify.reflexivity.
-elim y.simplify.reflexivity.
-elim z.simplify.reflexivity.
-change with
-eq Z (neg (pred (times (S (pred (times (S e1) (S e)))) (S e2))))
- (neg (pred (times (S e1) (S (pred (times (S e) (S e2))))))).
-rewrite < S_pred_S.
-
-theorem Zpred_Zplus_neg_O : \forall z:Z. eq Z (Zpred z) (Zplus (neg O) z).
-intros.elim z.
-simplify.reflexivity.
-simplify.reflexivity.
-elim e2.simplify.reflexivity.
-simplify.reflexivity.
-qed.
-
-theorem Zsucc_Zplus_pos_O : \forall z:Z. eq Z (Zsucc z) (Zplus (pos O) z).
-intros.elim z.
-simplify.reflexivity.
-elim e1.simplify.reflexivity.
-simplify.reflexivity.
-simplify.reflexivity.
-qed.
-
-theorem Zplus_pos_pos:
-\forall n,m. eq Z (Zplus (pos n) (pos m)) (Zplus (Zsucc (pos n)) (Zpred (pos m))).
+change with \forall x,y,z:Z. (x*y)*z = x*(y*z).
+intros.elim x.
+ simplify.reflexivity.
+ elim y.
+ simplify.reflexivity.
+ elim z.
+ simplify.reflexivity.
+ change with
+ pos (pred ((S (pred ((S n) * (S n1)))) * (S n2))) =
+ pos (pred ((S n) * (S (pred ((S n1) * (S n2)))))).
+ rewrite < S_pred.rewrite < S_pred.rewrite < assoc_times.reflexivity.
+ apply lt_O_times_S_S.apply lt_O_times_S_S.
+ change with
+ neg (pred ((S (pred ((S n) * (S n1)))) * (S n2))) =
+ neg (pred ((S n) * (S (pred ((S n1) * (S n2)))))).
+ rewrite < S_pred.rewrite < S_pred.rewrite < assoc_times.reflexivity.
+ apply lt_O_times_S_S.apply lt_O_times_S_S.
+ elim z.
+ simplify.reflexivity.
+ change with
+ neg (pred ((S (pred ((S n) * (S n1)))) * (S n2))) =
+ neg (pred ((S n) * (S (pred ((S n1) * (S n2)))))).
+ rewrite < S_pred.rewrite < S_pred.rewrite < assoc_times.reflexivity.
+ apply lt_O_times_S_S.apply lt_O_times_S_S.
+ change with
+ pos (pred ((S (pred ((S n) * (S n1)))) * (S n2))) =
+ pos(pred ((S n) * (S (pred ((S n1) * (S n2)))))).
+ rewrite < S_pred.rewrite < S_pred.rewrite < assoc_times.reflexivity.
+ apply lt_O_times_S_S.apply lt_O_times_S_S.
+ elim y.
+ simplify.reflexivity.
+ elim z.
+ simplify.reflexivity.
+ change with
+ neg (pred ((S (pred ((S n) * (S n1)))) * (S n2))) =
+ neg (pred ((S n) * (S (pred ((S n1) * (S n2)))))).
+ rewrite < S_pred.rewrite < S_pred.rewrite < assoc_times.reflexivity.
+ apply lt_O_times_S_S.apply lt_O_times_S_S.
+ change with
+ pos (pred ((S (pred ((S n) * (S n1)))) * (S n2))) =
+ pos (pred ((S n) * (S (pred ((S n1) * (S n2)))))).
+ rewrite < S_pred.rewrite < S_pred.rewrite < assoc_times.reflexivity.
+ apply lt_O_times_S_S.apply lt_O_times_S_S.
+ elim z.
+ simplify.reflexivity.
+ change with
+ pos (pred ((S (pred ((S n) * (S n1)))) * (S n2))) =
+ pos (pred ((S n) * (S (pred ((S n1) * (S n2)))))).
+ rewrite < S_pred.rewrite < S_pred.rewrite < assoc_times.reflexivity.
+ apply lt_O_times_S_S.apply lt_O_times_S_S.
+ change with
+ neg (pred ((S (pred ((S n) * (S n1)))) * (S n2))) =
+ neg(pred ((S n) * (S (pred ((S n1) * (S n2)))))).
+ rewrite < S_pred.rewrite < S_pred.rewrite < assoc_times.reflexivity.
+ apply lt_O_times_S_S.apply lt_O_times_S_S.
+qed.
+
+variant assoc_Ztimes : \forall x,y,z:Z.
+(x * y) * z = x * (y * z) \def
+associative_Ztimes.
+
+lemma times_minus1: \forall n,p,q:nat. lt q p \to
+(S n) * (S (pred ((S p) - (S q)))) =
+pred ((S n) * (S p)) - pred ((S n) * (S q)).