theorem associative_Ztimes: associative Z Ztimes.
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.
+intros.elim x.
+ simplify.reflexivity.
+ 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.
+ 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.
qed.
variant assoc_Ztimes : \forall x,y,z:Z.
distributive2 nat Z (\lambda n,z. Ztimes (pos n) z) Zplus.
change with \forall n,y,z.
eq Z (Ztimes (pos n) (Zplus y z)) (Zplus (Ztimes (pos n) y) (Ztimes (pos n) z)).
-intros.
-elim y.reflexivity.
-elim z.reflexivity.
-change with
-eq Z (neg (pred (times (S n) (plus (S n1) (S n2)))))
+intros.elim y.
+ reflexivity.
+ elim z.
+ reflexivity.
+ change with
+ eq Z (pos (pred (times (S n) (plus (S n1) (S n2)))))
+ (pos (pred (plus (times (S n) (S n1))(times (S n) (S n2))))).
+ rewrite < distr_times_plus.reflexivity.
+ apply Ztimes_Zplus_pos_pos_neg.
+ elim z.
+ reflexivity.
+ apply Ztimes_Zplus_pos_neg_pos.
+ change with
+ eq Z (neg (pred (times (S n) (plus (S n1) (S n2)))))
(neg (pred (plus (times (S n) (S n1))(times (S n) (S n2))))).
-rewrite < distr_times_plus.reflexivity.
-apply Ztimes_Zplus_pos_neg_pos.
-elim z.reflexivity.
-apply Ztimes_Zplus_pos_pos_neg.
-change with
-eq Z (pos (pred (times (S n) (plus (S n1) (S n2)))))
- (pos (pred (plus (times (S n) (S n1))(times (S n) (S n2))))).
-rewrite < distr_times_plus.
-reflexivity.
+ rewrite < distr_times_plus.reflexivity.
qed.
variant distr_Ztimes_Zplus_pos: \forall n,y,z.
intros.elim x.
(* case x = OZ *)
simplify.reflexivity.
-(* case x = neg n *)
-apply distr_Ztimes_Zplus_neg.
(* case x = pos n *)
apply distr_Ztimes_Zplus_pos.
+(* case x = neg n *)
+apply distr_Ztimes_Zplus_neg.
qed.
variant distr_Ztimes_Zplus: \forall x,y,z.