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 520e99ea8f1e7a7d58f0a964fdd9021076b17938..f79891b48a39b7394493d8cf7cc2cfa547450c81 100644 (file)
--- a/helm/matita/library/nat/div_and_mod.ma
+++ b/helm/matita/library/nat/div_and_mod.ma
@@ -144,7 +144,6 @@ rewrite > sym_times.
 rewrite < H5.
 rewrite < sym_times.
 apply plus_to_minus.
-apply eq_plus_to_le ? ? ? H3.
 apply H3.
 apply le_times_r.
 apply lt_to_le.
@@ -171,7 +170,6 @@ rewrite > sym_times.
 rewrite < H3.
 rewrite < sym_times.
 apply plus_to_minus.
-apply eq_plus_to_le ? ? ? H5.
 apply H5.
 apply le_times_r.
 apply lt_to_le.
@@ -212,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.
@@ -236,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).