Notation for "ex" introduced. It is the same as the notation for forall,

[helm.git] / helm / matita / library / nat / gcd.ma

diff --git a/helm/matita/library/nat/gcd.ma b/helm/matita/library/nat/gcd.ma
index 587314315268fc875ab715ab21ac83fd694c1613..b7ef49121cb2f77e39917294677a1dc9bcf192ec 100644 (file)
--- 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.
@@ -493,8 +490,7 @@ 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))).
+cut \exists a,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
@@ -504,8 +500,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.