+right.unfold Not.intro.apply H1.apply le_S_S_to_le.assumption.
+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.
+unfold monotonic.unfold lt.unfold increasing.unfold lt.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. unfold increasing in H.unfold lt in H.apply H.
+qed.
+
+theorem increasing_to_le: \forall f:nat \to nat. (increasing f)
+\to \forall m:nat. \exists 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.unfold increasing in H.unfold lt 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
+\exists 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.