X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fnat%2Fcongruence.ma;h=948d10667261ddc7971811c359f65424a0741aef;hb=a57ca0d68754b946b33976acf2e72f45ff11c8d7;hp=753745d4540d23f1378fcd3f4ac9cbc2791f14e0;hpb=c445ba5534cccde19016c92660ab52777af221c0;p=helm.git

diff --git a/helm/software/matita/library/nat/congruence.ma b/helm/software/matita/library/nat/congruence.ma
index 753745d45..948d10667 100644
--- a/helm/software/matita/library/nat/congruence.ma
+++ b/helm/software/matita/library/nat/congruence.ma
@@ -118,7 +118,7 @@ qed.
 theorem divides_to_congruent: \forall n,m,p:nat. O < p \to m \le n \to 
 divides p (n - m) \to congruent n m p.
 intros.elim H2.
-apply (eq_times_plus_to_congruent n m p n2).
+apply (eq_times_plus_to_congruent n m p n1).
 assumption.
 rewrite < sym_plus.
 apply minus_to_plus.assumption.