X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Farithmetics%2Fcongruence.ma;h=d9792b5ebbe3fd079b48548325e7e1235d98d39f;hb=1efc4c2c7be1e4aff0ccccabf905d45795b3865f;hp=e8f8a77328fcf2ef5fe2f61f4472e5d0a7ff940f;hpb=53452958508001e7af3090695b619fe92135fb9e;p=helm.git

diff --git a/matita/matita/lib/arithmetics/congruence.ma b/matita/matita/lib/arithmetics/congruence.ma
index e8f8a7732..d9792b5eb 100644
--- a/matita/matita/lib/arithmetics/congruence.ma
+++ b/matita/matita/lib/arithmetics/congruence.ma
@@ -37,7 +37,7 @@ theorem le_to_mod: ∀n,m:nat. n < m → n = n \mod m.
 qed.
 
 theorem mod_mod : ∀n,p:nat. O<p → n \mod p = (n \mod p) \mod p.
-#n #p #posp >(div_mod (n \mod p) p) in ⊢ (? ? % ?) 
+#n #p #posp >(div_mod (n \mod p) p) in ⊢ (? ? % ?); 
 >(eq_div_O ? p) // @lt_mod_m_m //
 qed.
 
@@ -79,9 +79,9 @@ qed.
 theorem congruent_to_divides: ∀n,m,p:nat.O < p → 
   n ≅_{p} m → p ∣ (n - m).
 #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 //
+>commutative_times >(div_mod n p) in ⊢ (??%?);
+>(div_mod m p) in ⊢ (??%?); <(commutative_plus (m \mod p))
+<congnm <(minus_plus ? (n \mod p)) <minus_plus_m_m //
 qed.
 
 theorem mod_times: ∀n,m,p:nat. O < p →