added a function to reorder the metasenv.

[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..811706867e4729f52f57ffd1d7f9183073c122f2 100644 (file)
--- a/helm/matita/library/nat/orders.ma
+++ b/helm/matita/library/nat/orders.ma
@@ -24,12 +24,19 @@ inductive le (n:nat) : nat \to Prop \def
 
 (*CSC: the URI must disappear: there is a bug now *)
 interpretation "natural 'less or equal to'" 'leq x y = (cic:/matita/nat/orders/le.ind#xpointer(1/1) x y).
+(*CSC: the URI must disappear: there is a bug now *)
+interpretation "natural 'neither less nor equal to'" 'nleq x y =
+  (cic:/matita/logic/connectives/Not.con
+    (cic:/matita/nat/orders/le.ind#xpointer(1/1) x y)).
 
 definition lt: nat \to nat \to Prop \def
 \lambda n,m:nat.(S n) \leq m.
 
 (*CSC: the URI must disappear: there is a bug now *)
 interpretation "natural 'less than'" 'lt x y = (cic:/matita/nat/orders/lt.con x y).
+(*CSC: the URI must disappear: there is a bug now *)
+interpretation "natural 'not less than'" 'nless x y =
+  (cic:/matita/logic/connectives/Not.con (cic:/matita/nat/orders/lt.con x y)).
 
 definition ge: nat \to nat \to Prop \def
 \lambda n,m:nat.m \leq n.
@@ -42,6 +49,9 @@ definition gt: nat \to nat \to Prop \def
 
 (*CSC: the URI must disappear: there is a bug now *)
 interpretation "natural 'greater than'" 'gt x y = (cic:/matita/nat/orders/gt.con x y).
+(*CSC: the URI must disappear: there is a bug now *)
+interpretation "natural 'not greater than'" 'ngtr x y =
+  (cic:/matita/logic/connectives/Not.con (cic:/matita/nat/orders/gt.con x y)).
 
 theorem transitive_le : transitive nat le.
 simplify.intros.elim H1.
@@ -248,3 +258,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.