X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fnat%2Fgcd.ma;h=3771bb6e56be891b628ed7991347ef2b63f5b92e;hb=f2bf34a07e2494d81ab7c3b44c143dec33e51fe8;hp=3db29f622fb95a5e096cb46744928c97bcef9f39;hpb=c445ba5534cccde19016c92660ab52777af221c0;p=helm.git

diff --git a/helm/software/matita/library/nat/gcd.ma b/helm/software/matita/library/nat/gcd.ma
index 3db29f622..3771bb6e5 100644
--- a/helm/software/matita/library/nat/gcd.ma
+++ b/helm/software/matita/library/nat/gcd.ma
@@ -55,7 +55,7 @@ qed.
 theorem divides_mod_to_divides: \forall p,m,n:nat. O < n \to
 p \divides (m \mod n) \to p \divides n \to p \divides m. 
 intros.elim H1.elim H2.
-apply (witness p m ((n1*(m / n))+n2)).
+apply (witness p m ((n2*(m / n))+n1)).
 rewrite > distr_times_plus.
 rewrite < H3.
 rewrite < assoc_times.
@@ -652,9 +652,9 @@ elim H2.
 generalize in match H1.
 rewrite > H3.
 intro.
-cut (O < n2)
-  [elim (gcd_times_SO_to_gcd_SO n n n2 ? ? H4)
-    [cut (gcd n (n*n2) = n)
+cut (O < n1)
+  [elim (gcd_times_SO_to_gcd_SO n n n1 ? ? H4)
+    [cut (gcd n (n*n1) = n)
       [apply (lt_to_not_eq (S O) n)
         [assumption|rewrite < H4.assumption]
       |apply gcd_n_times_nm.assumption
@@ -662,7 +662,7 @@ cut (O < n2)
     |apply (trans_lt ? (S O))[apply le_n|assumption]
     |assumption
     ]
-  |elim (le_to_or_lt_eq O n2 (le_O_n n2));
+  |elim (le_to_or_lt_eq O n1 (le_O_n n1));
     [assumption
     |apply False_ind.
      apply (le_to_not_lt n (S O))
@@ -670,7 +670,7 @@ cut (O < n2)
        apply divides_to_le
         [rewrite > H4.apply lt_O_S
         |apply divides_d_gcd
-          [apply (witness ? ? n2).reflexivity
+          [apply (witness ? ? n1).reflexivity
           |apply divides_n_n
           ]
         ]
@@ -784,7 +784,7 @@ cut (n \divides p \lor n \ndivides p)
           rewrite < (assoc_times q).
           rewrite < (sym_times n).
           rewrite < distr_times_minus.
-          apply (witness ? ? (n2*a1-q*a)).reflexivity
+          apply (witness ? ? (n1*a1-q*a)).reflexivity
         ](* end second case *)
      |rewrite < (prime_to_gcd_SO n p)
        [apply eq_minus_gcd|assumption|assumption
@@ -926,7 +926,7 @@ rewrite > H4 in H2.
 elim (divides_times_to_divides ? ? ? H H2)
   [apply False_ind.apply H1.assumption
   |elim H5.
-   apply (witness ? ? n1).
+   apply (witness ? ? n2).
    rewrite > sym_times in ⊢ (? ? ? (? % ?)).
    rewrite > assoc_times.
    rewrite < H6.assumption