- nnAuto.ml: width overflows are warnings, not errors

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

diff --git a/matita/matita/lib/arithmetics/congruence.ma b/matita/matita/lib/arithmetics/congruence.ma
index e8f8a77328fcf2ef5fe2f61f4472e5d0a7ff940f..d1afc19eec57ae6674c1d5e67e06e453ef88998d 100644 (file)
--- a/matita/matita/lib/arithmetics/congruence.ma
+++ b/matita/matita/lib/arithmetics/congruence.ma
@@ -81,7 +81,7 @@ theorem congruent_to_divides: ∀n,m,p:nat.O < p →
 #n #m #p #posp #congnm @(quotient ? ? ((n / p)-(m / p)))
 >commutative_times >(div_mod n p) in ⊢ (??%?)
 >(div_mod m p) in ⊢ (??%?) <(commutative_plus (m \mod p))
-<congnm <(minus_minus ? (n \mod p)) <minus_plus_m_m //
+<congnm <(minus_plus ? (n \mod p)) <minus_plus_m_m //
 qed.
 
 theorem mod_times: ∀n,m,p:nat. O < p →