Keeping track of locations of disambiguated ids and symbols.

[helm.git] / matita / matita / lib / arithmetics / primes.ma

diff --git a/matita/matita/lib/arithmetics/primes.ma b/matita/matita/lib/arithmetics/primes.ma
index 2c4897d06d00152d33bd03a98c1a810985f447f8..71e372f96722f893ebd3889a0b78eaf59f37d1fb 100644 (file)
--- a/matita/matita/lib/arithmetics/primes.ma
+++ b/matita/matita/lib/arithmetics/primes.ma
@@ -81,7 +81,7 @@ theorem eq_mod_to_divides: ∀n,m,q. O < q →
   |@(quotient ?? ((div n q)-(div m q)))
    >distributive_times_minus >commutative_times
    >(commutative_times q) cut((n/q)*q = n - (n \mod q)) [//] #H
-   >H >minus_minus >eqmod >commutative_plus 
+   >H >minus_plus >eqmod >commutative_plus 
    <div_mod //
   ]
 qed.