X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Flibrary%2Fnat%2Fgcd.ma;h=99c97b09add8d506bc1566c5250da6fd3b76969f;hb=7deb67bf075a845f84d51ac4757a5c69b779487d;hp=8475fc06aa026aacff1fd29c46c264ff25575947;hpb=adfeba63282f11f92705b61cb961a61e107fb5bb;p=helm.git

diff --git a/helm/matita/library/nat/gcd.ma b/helm/matita/library/nat/gcd.ma
index 8475fc06a..99c97b09a 100644
--- a/helm/matita/library/nat/gcd.ma
+++ b/helm/matita/library/nat/gcd.ma
@@ -297,6 +297,7 @@ rewrite < H7.
 apply ex_intro ? ? (a1+a*(div m n1)).
 apply ex_intro ? ? a.
 left.
+(* clear Hcut2.clear H5.clear H6.clear H. *)
 rewrite > sym_times.
 rewrite > distr_times_plus.
 rewrite > sym_times.
@@ -331,28 +332,7 @@ qed.
 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
-\exists a,b.
-a*n - b*m = 
-match leb n m with
-  [ true \Rightarrow 
-    match n with 
-    [ O \Rightarrow m
-    | (S p) \Rightarrow gcd_aux (S p) m (S p) ]
-  | false \Rightarrow 
-    match m with 
-    [ O \Rightarrow n
-    | (S p) \Rightarrow gcd_aux (S p) n (S p) ]]
-\lor b*m - a*n = 
-match leb n m with
-  [ true \Rightarrow 
-    match n with 
-    [ O \Rightarrow m
-    | (S p) \Rightarrow gcd_aux (S p) m (S p) ]
-  | false \Rightarrow 
-    match m with 
-    [ O \Rightarrow n
-    | (S p) \Rightarrow gcd_aux (S p) n (S p) ]].
+unfold gcd.
 apply leb_elim n m.
 apply nat_case1 n.
 simplify.intros.