A few changes to factorization and gcd.

[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 8475fc06aa026aacff1fd29c46c264ff25575947..99c97b09add8d506bc1566c5250da6fd3b76969f 100644 (file)
--- 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.