X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fnat%2Fdiv_and_mod.ma;h=cbab87206ee5457cf967e25505b3772ed9180b15;hb=e880d6eab5e1700f4a625ddcd7d0fa8f0cce2dcc;hp=fbf51276189b1524bb8418eb0f611606cd5f5f54;hpb=4dc47c9675ffd5fa50296ffaa9b5997501518c98;p=helm.git diff --git a/helm/software/matita/library/nat/div_and_mod.ma b/helm/software/matita/library/nat/div_and_mod.ma index fbf512761..cbab87206 100644 --- a/helm/software/matita/library/nat/div_and_mod.ma +++ b/helm/software/matita/library/nat/div_and_mod.ma @@ -147,11 +147,14 @@ apply le_plus_n. rewrite < sym_times. rewrite > distr_times_minus. rewrite > plus_minus. +lapply(plus_to_minus ??? H3); demodulate all. +(* rewrite > sym_times. rewrite < H5. rewrite < sym_times. apply plus_to_minus. apply H3. +*) apply le_times_r. apply lt_to_le. apply H6. @@ -195,8 +198,8 @@ qed. theorem div_mod_spec_times : \forall n,m:nat.div_mod_spec ((S n)*m) (S n) m O. intros.constructor 1. -unfold lt.apply le_S_S.apply le_O_n. -rewrite < plus_n_O.rewrite < sym_times.reflexivity. +unfold lt.apply le_S_S.apply le_O_n. demodulate. reflexivity. +(*rewrite < plus_n_O.rewrite < sym_times.reflexivity.*) qed. lemma div_plus_times: \forall m,q,r:nat. r < m \to (q*m+r)/ m = q. @@ -243,8 +246,8 @@ theorem div_n_n: \forall n:nat. O < n \to n / n = S O. intros. apply (div_mod_spec_to_eq n n (n / n) (n \mod n) (S O) O). apply div_mod_spec_div_mod.assumption. -constructor 1.assumption. -rewrite < plus_n_O.simplify.rewrite < plus_n_O.reflexivity. +constructor 1.assumption. demodulate. reflexivity. (* +rewrite < plus_n_O.simplify.rewrite < plus_n_O.reflexivity.*) qed. theorem eq_div_O: \forall n,m. n < m \to n / m = O. @@ -260,8 +263,8 @@ theorem mod_n_n: \forall n:nat. O < n \to n \mod n = O. intros. apply (div_mod_spec_to_eq2 n n (n / n) (n \mod n) (S O) O). apply div_mod_spec_div_mod.assumption. -constructor 1.assumption. -rewrite < plus_n_O.simplify.rewrite < plus_n_O.reflexivity. +constructor 1.assumption. demodulate. reflexivity.(* +rewrite < plus_n_O.simplify.rewrite < plus_n_O.reflexivity.*) qed. theorem mod_S: \forall n,m:nat. O < m \to S (n \mod m) < m \to