added hmysql

[helm.git] / helm / matita / library / nat / div_and_mod.ma

diff --git a/helm/matita/library/nat/div_and_mod.ma b/helm/matita/library/nat/div_and_mod.ma
index 71734fad3a58ff17c619da36325bbd13dca6c415..f79891b48a39b7394493d8cf7cc2cfa547450c81 100644 (file)
--- 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).