-
-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.
-simplify.
-apply le_SO_minus. exact H.
-intro.rewrite < H.simplify.reflexivity.
-intro.
-change with (eq Z (pos (pred (times (S n) (S (pred (minus (S n1) (S n2)))))))
- (pos (pred (minus (pred (times (S n) (S n1)))
- (pred (times (S n) (S n2))))))).
+lemma times_minus1: \forall n,p,q:nat. lt q p \to
+eq nat (times (S n) (S (pred (minus (S p) (S q)))))
+ (minus (pred (times (S n) (S p)))
+ (pred (times (S n) (S q)))).
+intros.