New entry: relevant_equations.

[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..26e3dcc829a604fa0b1453fe249928a2dac154dd 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.