(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/nat/orders".
-
include "nat/nat.ma".
include "higher_order_defs/ordering.ma".
| le_n : le n n
| le_S : \forall m:nat. le n m \to le n (S m).
-interpretation "natural 'less or equal to'" 'leq x y = (cic:/matita/nat/orders/le.ind#xpointer(1/1) x y).
+interpretation "natural 'less or equal to'" 'leq x y = (le x y).
-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)).
+interpretation "natural 'neither less nor equal to'" 'nleq x y = (Not (le x y)).
definition lt: nat \to nat \to Prop \def
\lambda n,m:nat.(S n) \leq m.
-interpretation "natural 'less than'" 'lt x y = (cic:/matita/nat/orders/lt.con x y).
+interpretation "natural 'less than'" 'lt x y = (lt x y).
-interpretation "natural 'not less than'" 'nless x y =
- (cic:/matita/logic/connectives/Not.con (cic:/matita/nat/orders/lt.con x y)).
+interpretation "natural 'not less than'" 'nless x y = (Not (lt x y)).
definition ge: nat \to nat \to Prop \def
\lambda n,m:nat.m \leq n.
-interpretation "natural 'greater or equal to'" 'geq x y = (cic:/matita/nat/orders/ge.con x y).
+interpretation "natural 'greater or equal to'" 'geq x y = (ge x y).
definition gt: nat \to nat \to Prop \def
\lambda n,m:nat.m<n.
-interpretation "natural 'greater than'" 'gt x y = (cic:/matita/nat/orders/gt.con x y).
+interpretation "natural 'greater than'" 'gt x y = (gt x y).
-interpretation "natural 'not greater than'" 'ngtr x y =
- (cic:/matita/logic/connectives/Not.con (cic:/matita/nat/orders/gt.con x y)).
+interpretation "natural 'not greater than'" 'ngtr x y = (Not (gt x y)).
theorem transitive_le : transitive nat le.
unfold transitive.intros.elim H1.
[ simplify;
apply le_O_n
| simplify;
- generalize in match H1;
- clear H1;
- elim m;
+ elim m in H1 ⊢ %;
[ elim (not_le_Sn_O ? H1)
| simplify;
apply le_S_S_to_le;
apply le_O_n.assumption.
qed.
+theorem lt_SO_n_to_lt_O_pred_n: \forall n:nat.
+(S O) \lt n \to O \lt (pred n).
+intros.
+apply (ltn_to_ltO (pred (S O)) (pred n) ?).
+ apply (lt_pred (S O) n);
+ [ apply (lt_O_S O)
+ | assumption
+ ]
+qed.
+
theorem lt_O_n_elim: \forall n:nat. lt O n \to
\forall P:nat\to Prop. (\forall m:nat.P (S m)) \to P n.
intro.elim n.apply False_ind.exact (not_le_Sn_O O H).