fixed a finalization issue for connections closed twice

[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 4ec4dfc5b11089876cafc3d2802a80f098c3917a..d592ed0afa4951d6d080109771eab40923568984 100644 (file)
--- a/helm/matita/library/nat/orders.ma
+++ b/helm/matita/library/nat/orders.ma
@@ -104,6 +104,14 @@ apply H.assumption.
 apply le_S_S_to_le.assumption.
 qed.
 
+(* le to lt or eq *)
+theorem le_to_or_lt_eq : \forall n,m:nat. 
+n \leq m \to n < m \lor n = m.
+intros.elim H.
+right.reflexivity.
+left.simplify.apply le_S_S.assumption.
+qed.
+
 (* not eq *)
 theorem lt_to_not_eq : \forall n,m:nat. n<m \to \lnot (n=m).
 simplify.intros.cut (le (S n) m) \to False.
@@ -224,3 +232,71 @@ qed.
 theorem decidable_lt: \forall n,m:nat. decidable (n < m).
 intros.exact decidable_le (S n) m.
 qed.
+
+(* well founded induction principles *)
+
+theorem nat_elim1 : \forall n:nat.\forall P:nat \to Prop. 
+(\forall m.(\forall p. (p \lt m) \to P p) \to P m) \to P n.
+intros.cut \forall q:nat. q \le n \to P q.
+apply Hcut n.apply le_n.
+elim n.apply le_n_O_elim q H1.
+apply H.
+intros.apply False_ind.apply not_le_Sn_O p H2.
+apply H.intros.apply H1.
+cut p < S n1.
+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.