New version of the library. nth_prime, gcd, log.

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

diff --git a/helm/matita/library/nat/lt_arith.ma b/helm/matita/library/nat/lt_arith.ma
index 9494a28d7983b9735d8f04e58d00db58512da77a..85280fe0f2da8aef41e9e030c42428b82d30f7ea 100644 (file)
--- a/helm/matita/library/nat/lt_arith.ma
+++ b/helm/matita/library/nat/lt_arith.ma
@@ -14,6 +14,7 @@
 
 set "baseuri" "cic:/matita/nat/lt_arith".
 
+include "nat/exp.ma".
 include "nat/div_and_mod.ma".
 
 (* plus *)
@@ -161,3 +162,58 @@ apply lt_to_not_eq.assumption.
 intro.reflexivity.
 qed.
 
+(* div *) 
+
+theorem eq_mod_O_to_lt_O_div: \forall n,m:nat. O < m \to O < n\to mod n m = O \to O < div n m. 
+intros 4.apply lt_O_n_elim m H.intros.
+apply lt_times_to_lt_r m1.
+rewrite < times_n_O.
+rewrite > plus_n_O ((S m1)*(div n (S m1))).
+rewrite < H2.
+rewrite < sym_times.
+rewrite < div_mod.
+rewrite > H2.
+assumption.
+simplify.apply le_S_S.apply le_O_n.
+qed.
+
+theorem lt_div_n_m_n: \forall n,m:nat. (S O) < m \to O < n \to div n m \lt n.
+intros.
+apply nat_case1 (div n m).intro.
+assumption.intros.rewrite < H2.
+rewrite > (div_mod n m) in \vdash (? ? %).
+apply lt_to_le_to_lt ? ((div n m)*m).
+apply lt_to_le_to_lt ? ((div n m)*(S (S O))).
+rewrite < sym_times.
+rewrite > H2.
+simplify.
+rewrite < plus_n_O.
+rewrite < plus_n_Sm.
+apply le_S_S.
+apply le_S_S.
+apply le_plus_n.
+apply le_times_r.
+assumption.
+rewrite < sym_plus.
+apply le_plus_n.
+apply trans_lt ? (S O).
+simplify. apply le_n.assumption.
+qed.
+
+(* general properties of functions *)
+theorem monotonic_to_injective: \forall f:nat\to nat.
+monotonic nat lt f \to injective nat nat f.
+simplify.intros.
+apply nat_compare_elim x y.
+intro.apply False_ind.apply not_le_Sn_n (f x).
+rewrite > H1 in \vdash (? ? %).apply H.apply H2.
+intros.assumption.
+intro.apply False_ind.apply not_le_Sn_n (f y).
+rewrite < H1 in \vdash (? ? %).apply H.apply H2.
+qed.
+
+theorem increasing_to_injective: \forall f:nat\to nat.
+increasing f \to injective nat nat f.
+intros.apply monotonic_to_injective.
+apply increasing_to_monotonic.assumption.
+qed.
\ No newline at end of file