X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Flibrary%2Fnat%2Fgcd.ma;h=be1d79b1d265c3fb50f059015b8a5fda4058f1f1;hb=2ecd65dbcc1388bb2dfe6425e6ef1b2e3f45c4ac;hp=587314315268fc875ab715ab21ac83fd694c1613;hpb=5a702cea95883f7095c16b450e065ccb1714fc5a;p=helm.git

diff --git a/helm/matita/library/nat/gcd.ma b/helm/matita/library/nat/gcd.ma
index 587314315..be1d79b1d 100644
--- a/helm/matita/library/nat/gcd.ma
+++ b/helm/matita/library/nat/gcd.ma
@@ -243,22 +243,21 @@ rewrite < H2.assumption.
 qed.
 
 theorem eq_minus_gcd_aux: \forall p,m,n.O < n \to n \le m \to n \le p \to
-ex nat (\lambda a. ex nat (\lambda b.
-a*n - b*m = (gcd_aux p m n) \lor b*m - a*n = (gcd_aux p m n))).
+\exists a,b. a*n - b*m = gcd_aux p m n \lor b*m - a*n = gcd_aux p m n.
 intro.
 elim p.
 absurd O < n.assumption.apply le_to_not_lt.assumption.
 cut O < m.
 cut (divides n1 m) \lor \not (divides n1 m).
 change with
-ex nat (\lambda a. ex nat (\lambda b.
+\exists a,b.
 a*n1 - b*m = match divides_b n1 m with
 [ true \Rightarrow n1
 | false \Rightarrow gcd_aux n n1 (mod m n1)]
 \lor 
 b*m - a*n1 = match divides_b n1 m with
 [ true \Rightarrow n1
-| false \Rightarrow gcd_aux n n1 (mod m n1)])).
+| false \Rightarrow gcd_aux n n1 (mod m n1)].
 elim Hcut1.
 rewrite > divides_to_divides_b_true.
 simplify.
@@ -269,15 +268,15 @@ apply sym_eq.apply minus_n_O.
 assumption.assumption.
 rewrite > not_divides_to_divides_b_false.
 change with
-ex nat (\lambda a. ex nat (\lambda b.
+\exists a,b.
 a*n1 - b*m = gcd_aux n n1 (mod m n1)
 \lor 
-b*m - a*n1 = gcd_aux n n1 (mod m n1))).
+b*m - a*n1 = gcd_aux n n1 (mod m n1).
 cut 
-ex nat (\lambda a. ex nat (\lambda b.
+\exists a,b.
 a*(mod m n1) - b*n1= gcd_aux n n1 (mod m n1)
 \lor
-b*n1 - a*(mod m n1) = gcd_aux n n1 (mod m n1))).
+b*n1 - a*(mod m n1) = gcd_aux n n1 (mod m n1).
 elim Hcut2.elim H5.elim H6.
 (* first case *)
 rewrite < H7.
@@ -335,12 +334,11 @@ apply decidable_divides n1 m.assumption.
 apply lt_to_le_to_lt ? n1.assumption.assumption.
 qed.
 
-theorem eq_minus_gcd: \forall m,n.
-ex nat (\lambda a. ex nat (\lambda b.
-a*n - b*m = (gcd n m) \lor b*m - a*n = (gcd n m))).
+theorem eq_minus_gcd:
+ \forall m,n.\exists a,b.a*n - b*m = (gcd n m) \lor b*m - a*n = (gcd n m).
 intros.
 change with
-ex nat (\lambda a. ex nat (\lambda b.
+\exists a,b.
 a*n - b*m = 
 match leb n m with
   [ true \Rightarrow 
@@ -360,8 +358,7 @@ match leb n m with
   | false \Rightarrow 
     match m with 
     [ O \Rightarrow n
-    | (S p) \Rightarrow gcd_aux (S p) n (S p) ]]
-)).
+    | (S p) \Rightarrow gcd_aux (S p) n (S p) ]].
 apply leb_elim n m.
 apply nat_case1 n.
 simplify.intros.
@@ -372,9 +369,9 @@ rewrite < plus_n_O.
 apply sym_eq.apply minus_n_O.
 intros.
 change with 
-ex nat (\lambda a. ex nat (\lambda b.
+\exists a,b.
 a*(S m1) - b*m = (gcd_aux (S m1) m (S m1)) 
-\lor b*m - a*(S m1) = (gcd_aux (S m1) m (S m1)))).
+\lor b*m - a*(S m1) = (gcd_aux (S m1) m (S m1)).
 apply eq_minus_gcd_aux.
 simplify. apply le_S_S.apply le_O_n.
 assumption.apply le_n.
@@ -387,14 +384,14 @@ rewrite < plus_n_O.
 apply sym_eq.apply minus_n_O.
 intros.
 change with 
-ex nat (\lambda a. ex nat (\lambda b.
+\exists a,b.
 a*n - b*(S m1) = (gcd_aux (S m1) n (S m1)) 
-\lor b*(S m1) - a*n = (gcd_aux (S m1) n (S m1)))).
+\lor b*(S m1) - a*n = (gcd_aux (S m1) n (S m1)).
 cut 
-ex nat (\lambda a. ex nat (\lambda b.
+\exists a,b.
 a*(S m1) - b*n = (gcd_aux (S m1) n (S m1))
 \lor
-b*n - a*(S m1) = (gcd_aux (S m1) n (S m1)))).
+b*n - a*(S m1) = (gcd_aux (S m1) n (S m1)).
 elim Hcut.elim H2.elim H3.
 apply ex_intro ? ? a1.
 apply ex_intro ? ? a.
@@ -485,18 +482,6 @@ apply gcd_O_to_eq_O.apply sym_eq.assumption.
 apply le_to_or_lt_eq.apply le_O_n.
 qed.
 
-(* esempio di sfarfallalmento !!! *)
-(*
-theorem bad: \forall n,p,q:nat.prime n \to divides n (p*q) \to
-divides n p \lor divides n q.
-intros.
-cut divides n p \lor \not (divides n p).
-elim Hcut.left.assumption.
-right.
-cut ex nat (\lambda a. ex nat (\lambda b.
-a*n - b*p = (S O) \lor b*p - a*n = (S O))).
-elim Hcut1.elim H3.*)
-
 theorem divides_times_to_divides: \forall n,p,q:nat.prime n \to divides n (p*q) \to
 divides n p \lor divides n q.
 intros.
@@ -504,8 +489,7 @@ cut divides n p \lor \not (divides n p).
 elim Hcut.
 left.assumption.
 right.
-cut ex nat (\lambda a. ex nat (\lambda b.
-a*n - b*p = (S O) \lor b*p - a*n = (S O))).
+cut \exists a,b. a*n - b*p = (S O) \lor b*p - a*n = (S O).
 elim Hcut1.elim H3.elim H4.
 (* first case *)
 rewrite > times_n_SO q.rewrite < H5.