The library grows...

[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..122aebcfa41c21cdb537cbf71a18c848c989835b 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,19 @@ 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.
+