X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Flibrary%2Fnat%2Fdiv_and_mod.ma;h=f79891b48a39b7394493d8cf7cc2cfa547450c81;hb=aeb7f0539398561dc84cadf38df14a051dd1ba75;hp=71734fad3a58ff17c619da36325bbd13dca6c415;hpb=7273c698dd60c1a8a0f35b44376acb548c6a4a33;p=helm.git

diff --git a/helm/matita/library/nat/div_and_mod.ma b/helm/matita/library/nat/div_and_mod.ma
index 71734fad3..f79891b48 100644
--- a/helm/matita/library/nat/div_and_mod.ma
+++ b/helm/matita/library/nat/div_and_mod.ma
@@ -210,6 +210,15 @@ constructor 1.assumption.
 rewrite < plus_n_O.simplify.rewrite < plus_n_O.reflexivity.
 qed.
 
+theorem eq_div_O: \forall n,m. n < m \to n / m = O.
+intros.
+apply div_mod_spec_to_eq n m (n/m) (n \mod m) O n.
+apply div_mod_spec_div_mod.
+apply le_to_lt_to_lt O n m.
+apply le_O_n.assumption.
+constructor 1.assumption.reflexivity.
+qed.
+
 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.
@@ -234,6 +243,14 @@ intro.elim n.simplify.reflexivity.
 simplify.reflexivity.
 qed.
 
+theorem lt_to_eq_mod:\forall n,m:nat. n < m \to n \mod m = n.
+intros.
+apply div_mod_spec_to_eq2 n m (n/m) (n \mod m) O n.
+apply div_mod_spec_div_mod.
+apply le_to_lt_to_lt O n m.apply le_O_n.assumption.
+constructor 1.
+assumption.reflexivity.
+qed.
 
 (* injectivity *)
 theorem injective_times_r: \forall n:nat.injective nat nat (\lambda m:nat.(S n)*m).