-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 n) (S n1)))) (S n2))))
- (neg (pred (times (S n) (S (pred (times (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
-eq Z (pos (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
- (pos (pred (times (S n) (S (pred (times (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
-eq Z (pos (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
- (pos(pred (times (S n) (S (pred (times (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
-eq Z (neg (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
- (neg (pred (times (S n) (S (pred (times (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
-eq Z (pos (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
- (pos (pred (times (S n) (S (pred (times (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
-eq Z (neg (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
- (neg (pred (times (S n) (S (pred (times (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
-eq Z (neg (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
- (neg(pred (times (S n) (S (pred (times (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
-eq Z (pos (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
- (pos (pred (times (S n) (S (pred (times (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 (\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.