-theorem decidable_le: ∀n,m. decidable (n≤m).
-@nat_elim2 #n /2/ #m * /3/ qed.
-
-theorem decidable_lt: ∀n,m. decidable (n < m).
-#n #m @decidable_le qed.
-
-theorem not_le_Sn_n: ∀n:nat. S n ≰ n.
-#n (elim n) /2/ qed.
-
-(* this is le_S_S_to_le
-theorem lt_S_to_le: ∀n,m:nat. n < S m → n ≤ m.
-/2/ qed.
-*)
-
-lemma le_gen: ∀P:nat → Prop.∀n.(∀i. i ≤ n → P i) → P n.
-/2/ qed.
-
-theorem not_le_to_lt: ∀n,m. n ≰ m → m < n.
-@nat_elim2 #n
- [#abs @False_ind /2/
- |/2/
- |#m #Hind #HnotleSS @le_S_S /3/
- ]
-qed.
-
-theorem lt_to_not_le: ∀n,m. n < m → m ≰ n.
-#n #m #Hltnm (elim Hltnm) /3/ qed.
-
-theorem not_lt_to_le: ∀n,m:nat. n ≮ m → m ≤ n.
-/4/ qed.
-
-theorem le_to_not_lt: ∀n,m:nat. n ≤ m → m ≮ n.
-#n #m #H @lt_to_not_le /2/ (* /3/ *) qed.
-
-(* lt and le trans *)
-
-theorem lt_to_le_to_lt: ∀n,m,p:nat. n < m → m ≤ p → n < p.
-#n #m #p #H #H1 (elim H1) /2/ qed.
-
-theorem le_to_lt_to_lt: ∀n,m,p:nat. n ≤ m → m < p → n < p.
-#n #m #p #H (elim H) /3/ qed.
-
-theorem lt_S_to_lt: ∀n,m. S n < m → n < m.
-/2/ qed.
-
-theorem ltn_to_ltO: ∀n,m:nat. n < m → O < m.
-/2/ 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: ∀n:nat. O < n →
- ∀P:nat → Prop.(∀m:nat.P (S m)) → P n.
-#n (elim n) // #abs @False_ind /2/
-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.
-
-theorem S_pred: \forall n:nat.lt O n \to eq nat n (S (pred n)).
-intro.elim n.apply False_ind.exact (not_le_Sn_O O H).
-apply eq_f.apply pred_Sn.
-qed.
-
-theorem le_pred_to_le:
- ∀n,m. O < m → pred n ≤ pred m → n ≤ m.
-intros 2
-elim n
-[ apply le_O_n
-| simplify in H2
- rewrite > (S_pred m)
- [ apply le_S_S
- assumption
- | assumption
- ]
-].
-qed.
-
-*)
-
-(* le to lt or eq *)
-theorem le_to_or_lt_eq: ∀n,m:nat. n ≤ m → n < m ∨ n = m.
-#n #m #lenm (elim lenm) /3/ qed.
-
-(* not eq *)
-theorem lt_to_not_eq : ∀n,m:nat. n < m → n ≠ m.
-#n #m #H @not_to_not /2/ qed.
-
-(*not lt
-theorem eq_to_not_lt: ∀a,b:nat. a = b → a ≮ b.
-intros.
-unfold Not.
-intros.
-rewrite > H in H1.
-apply (lt_to_not_eq b b)
-[ assumption
-| reflexivity
-]
-qed.
-
-theorem lt_n_m_to_not_lt_m_Sn: ∀n,m. n < m → m ≮ S n.
-intros
-unfold Not
-intro
-unfold lt in H
-unfold lt in H1
-generalize in match (le_S_S ? ? H)
-intro
-generalize in match (transitive_le ? ? ? H2 H1)
-intro
-apply (not_le_Sn_n ? H3).
-qed. *)
-
-theorem not_eq_to_le_to_lt: ∀n,m. n≠m → n≤m → n<m.
-#n #m #Hneq #Hle cases (le_to_or_lt_eq ?? Hle) //
-#Heq /3/ qed.
-(*
-nelim (Hneq Heq) qed. *)
-
-(* le elimination *)
-theorem le_n_O_to_eq : ∀n:nat. n ≤ O → O=n.
-#n (cases n) // #a #abs @False_ind /2/ qed.
-
-theorem le_n_O_elim: ∀n:nat. n ≤ O → ∀P: nat →Prop. P O → P n.
-#n (cases n) // #a #abs @False_ind /2/ qed.
-
-theorem le_n_Sm_elim : ∀n,m:nat.n ≤ S m →
-∀P:Prop. (S n ≤ S m → P) → (n=S m → P) → P.
-#n #m #Hle #P (elim Hle) /3/ qed.
-
-(* le and eq *)
-
-theorem le_to_le_to_eq: ∀n,m. n ≤ m → m ≤ n → n = m.
-@nat_elim2 /4/
-qed.
-
-theorem lt_O_S : ∀n:nat. O < S n.
-/2/ qed.
-
-(*
-(* other abstract properties *)
-theorem antisymmetric_le : antisymmetric nat le.
-unfold antisymmetric.intros 2.
-apply (nat_elim2 (\lambda n,m.(n \leq m \to m \leq n \to n=m))).
-intros.apply le_n_O_to_eq.assumption.
-intros.apply False_ind.apply (not_le_Sn_O ? H).
-intros.apply eq_f.apply H.
-apply le_S_S_to_le.assumption.
-apply le_S_S_to_le.assumption.
-qed.
-
-theorem antisym_le: \forall n,m:nat. n \leq m \to m \leq n \to n=m
-\def antisymmetric_le.
-
-theorem le_n_m_to_lt_m_Sn_to_eq_n_m: ∀n,m. n ≤ m → m < S n → n=m.
-intros
-unfold lt in H1
-generalize in match (le_S_S_to_le ? ? H1)
-intro
-apply antisym_le
-assumption.
-qed.
-*)
-
-(* well founded induction principles *)
-
-theorem nat_elim1 : ∀n:nat.∀P:nat → Prop.
-(∀m.(∀p. p < m → P p) → P m) → P n.
-#n #P #H
-cut (∀q:nat. q ≤ n → P q) /2/
-(elim n)
- [#q #HleO (* applica male *)
- @(le_n_O_elim ? HleO)
- @H #p #ltpO @False_ind /2/ (* 3 *)
- |#p #Hind #q #HleS
- @H #a #lta @Hind @le_S_S_to_le /2/
- ]
-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.
-qed.
-*)
-
-(*********************** monotonicity ***************************)