| le_n : le n n
| le_S : \forall m:nat. le n m \to le n (S m).
-(*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.
-(*CSC: the URI must disappear: there is a bug now *)
interpretation "natural 'greater or equal to'" 'geq x y = (cic:/matita/nat/orders/ge.con x y).
definition gt: nat \to nat \to Prop \def
\lambda n,m:nat.m<n.
-(*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)).
apply le_pred_n.
qed.
+theorem lt_S_S_to_lt: \forall n,m.
+ S n < S m \to n < m.
+intros. apply le_S_S_to_le. assumption.
+qed.
+
theorem leS_to_not_zero : \forall n,m:nat. S n \leq m \to not_zero m.
intros.elim H.exact I.exact I.
qed.
apply le_S_S_to_le.assumption.
qed.
+theorem lt_pred: \forall n,m.
+ O < n \to n < m \to pred n < pred m.
+apply nat_elim2
+ [intros.apply False_ind.apply (not_le_Sn_O ? H)
+ |intros.apply False_ind.apply (not_le_Sn_O ? H1)
+ |intros.simplify.unfold.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.
apply not_le_Sn_n.
qed.
+(*not lt*)
+theorem eq_to_not_lt: \forall a,b:nat.
+a = b \to a \nlt b.
+intros.
+unfold Not.
+intros.
+rewrite > H in H1.
+apply (lt_to_not_eq b b)
+[ assumption
+| reflexivity
+]
+qed.
+
(* le vs. lt *)
theorem lt_to_le : \forall n,m:nat. n<m \to n \leq m.
simplify.intros.unfold lt in H.elim H.
theorem le_n_O_to_eq : \forall n:nat. n \leq O \to O=n.
intro.elim n.reflexivity.
apply False_ind.
-apply not_le_Sn_O.
-goal 17. apply H1.
+apply not_le_Sn_O;
+[2: apply H1 | skip].
qed.
theorem le_n_O_elim: \forall n:nat.n \leq O \to \forall P: nat \to Prop.
apply H3. apply le_S_S. assumption.
qed.
-(* le to eq *)
+(* le and eq *)
lemma le_to_le_to_eq: \forall n,m. n \le m \to m \le n \to n = m.
apply nat_elim2
[intros.apply le_n_O_to_eq.assumption