Several changes. Proof of Fermat's little theorem completed.

[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 26e3dcc829a604fa0b1453fe249928a2dac154dd..f79891b48a39b7394493d8cf7cc2cfa547450c81 100644 (file)
--- a/helm/matita/library/nat/div_and_mod.ma
+++ b/helm/matita/library/nat/div_and_mod.ma
@@ -243,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).