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

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

diff --git a/helm/matita/library/nat/orders.ma b/helm/matita/library/nat/orders.ma
index 122aebcfa41c21cdb537cbf71a18c848c989835b..d592ed0afa4951d6d080109771eab40923568984 100644 (file)
--- a/helm/matita/library/nat/orders.ma
+++ b/helm/matita/library/nat/orders.ma
@@ -248,3 +248,55 @@ apply lt_S_to_le.assumption.
 apply lt_to_le_to_lt p q (S n1) H3 H2.
 qed.
 
+(* some properties of functions *)
+
+definition increasing \def \lambda f:nat \to nat. 
+\forall n:nat. f n < f (S n).
+
+theorem increasing_to_monotonic: \forall f:nat \to nat.
+increasing f \to monotonic nat lt f.
+simplify.intros.elim H1.apply H.
+apply trans_le ? (f n1).
+assumption.apply trans_le ? (S (f n1)).
+apply le_n_Sn.
+apply H.
+qed.
+
+theorem le_n_fn: \forall f:nat \to nat. (increasing f) 
+\to \forall n:nat. n \le (f n).
+intros.elim n.
+apply le_O_n.
+apply trans_le ? (S (f n1)).
+apply le_S_S.apply H1.
+simplify in H. apply H.
+qed.
+
+theorem increasing_to_le: \forall f:nat \to nat. (increasing f) 
+\to \forall m:nat. ex nat (\lambda i. m \le (f i)).
+intros.elim m.
+apply ex_intro ? ? O.apply le_O_n.
+elim H1.
+apply ex_intro ? ? (S a).
+apply trans_le ? (S (f a)).
+apply le_S_S.assumption.
+simplify in H.
+apply H.
+qed.
+
+theorem increasing_to_le2: \forall f:nat \to nat. (increasing f) 
+\to \forall m:nat. (f O) \le m \to 
+ex nat (\lambda i. (f i) \le m \land m <(f (S i))).
+intros.elim H1.
+apply ex_intro ? ? O.
+split.apply le_n.apply H.
+elim H3.elim H4.
+cut (S n1) < (f (S a)) \lor (S n1) = (f (S a)).
+elim Hcut.
+apply ex_intro ? ? a.
+split.apply le_S. assumption.assumption.
+apply ex_intro ? ? (S a).
+split.rewrite < H7.apply le_n.
+rewrite > H7.
+apply H.
+apply le_to_or_lt_eq.apply H6.
+qed.