+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.
+qed.
+
+variant assoc_Ztimes : \forall x,y,z:Z.
+eq Z (Ztimes (Ztimes x y) z) (Ztimes x (Ztimes y z)) \def
+associative_Ztimes.
+
+
+theorem distributive_Ztimes: distributive Z Ztimes Zplus.
+change with \forall x,y,z:Z.
+eq Z (Ztimes x (Zplus y z)) (Zplus (Ztimes x y) (Ztimes x z)).
+intros.elim x.
+simplify.reflexivity.
+(* case x = neg n *)
+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 < times_plus_distr.reflexivity.
+simplify. (* problemi di naming su n *)
+(* sintassi della change ??? *)
+cut \forall n,m:nat.eq nat (plus m (times n (S m))) (pred (times (S n) (S m))).
+rewrite > Hcut.
+rewrite > Hcut.
+rewrite < nat_compare_pred_pred ? ? ? ?.
+rewrite < nat_compare_times_l.
+rewrite < nat_compare_S_S.
+apply nat_compare_elim n1 n2.
+intro.
+(* per ricavare questo change ci ho messo un'ora;
+LA GESTIONE DELLA RIDUZIONE NON VA *)
+change with (eq Z (neg (pred (times (S n) (S (pred (minus (S n2) (S n1)))))))
+ (neg (pred (minus (pred (times (S n) (S n2)))
+ (pred (times (S n) (S n1))))))).
+rewrite < S_pred ? ?.
+rewrite > minus_pred_pred ? ? ? ?.
+rewrite < distr_times_minus.
+reflexivity.
+(* we start closing stupid positivity conditions *)
+apply lt_O_times_S_S.
+apply lt_O_times_S_S.