...

[helm.git] / helm / software / matita / library / nat / gcd_properties1.ma

diff --git a/helm/software/matita/library/nat/gcd_properties1.ma b/helm/software/matita/library/nat/gcd_properties1.ma
index bb8b9bb534881a1c019558c9212310bc669f2c72..8174465c60a27ab06b994e2278416f45b6463f91 100644 (file)
--- a/helm/software/matita/library/nat/gcd_properties1.ma
+++ b/helm/software/matita/library/nat/gcd_properties1.ma
@@ -12,8 +12,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/nat/gcd_properties1".
-
 include "nat/gcd.ma".
 
 (* this file contains some important properites of gcd in N *)
@@ -25,7 +23,7 @@ c \divides a \to c \divides b \to
 intros.
 elim (H2 ((gcd a b)))
 [ apply (antisymmetric_divides (gcd a b) c)
-  [ apply (witness (gcd a b) c n2).
+  [ apply (witness (gcd a b) c n1).
     assumption
   | apply divides_d_gcd;
       assumption
@@ -164,7 +162,7 @@ apply (nat_case1 a)
           ]
         | assumption
         ]
-      | apply (witness ? ? n2).
+      | apply (witness ? ? n1).
         apply (inj_times_r1 (gcd a b) Hcut1).
         rewrite < assoc_times.
         rewrite < sym_times in \vdash (? ? (? % ?) ?).
@@ -328,13 +326,13 @@ apply gcd1
 | intros.
   elim H1.
   elim H2.
-  cut(b = (d*n2) + a) 
-  [ cut (b - (d*n2) = a)
+  cut(b = (d*n1) + a) 
+  [ cut (b - (d*n1) = a)
     [ rewrite > H4 in Hcut1.
-      rewrite < (distr_times_minus d n n2) in Hcut1.
+      rewrite < (distr_times_minus d n n1) in Hcut1.
       apply divides_d_gcd
       [ assumption
-      | apply (witness d a (n - n2)).
+      | apply (witness d a (n - n1)).
         apply sym_eq.
         assumption
       ]