X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Farithmetics%2Fcongruence.ma;h=d9792b5ebbe3fd079b48548325e7e1235d98d39f;hb=1efc4c2c7be1e4aff0ccccabf905d45795b3865f;hp=2a9e06b0fabd6a47304d544bcb523c83e7af0724;hpb=ddc80515997a3f56085c6234d4db326141e189aa;p=helm.git diff --git a/matita/matita/lib/arithmetics/congruence.ma b/matita/matita/lib/arithmetics/congruence.ma index 2a9e06b0f..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
(div_mod (n \mod p) p) {⢠(? ? % ?) }
+#n #p #posp >(div_mod (n \mod p) p) in ⢠(? ? % ?);
>(eq_div_O ? p) // @lt_mod_m_m //
qed.
@@ -79,8 +79,8 @@ 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) {⢠(??%?)}
->(div_mod m p) {⢠(??%?)} <(commutative_plus (m \mod p))
+>commutative_times >(div_mod n p) in ⢠(??%?);
+>(div_mod m p) in ⢠(??%?); <(commutative_plus (m \mod p))