-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 ≝ λf:nat → nat. ∀n:nat. f n < f (S n).
-
-theorem increasing_to_monotonic: ∀f:nat → nat.
- increasing f → monotonic nat lt f.
-#f #incr #n #m #ltnm (elim ltnm) /2/
-qed.
-
-theorem le_n_fn: ∀f:nat → nat.
- increasing f → ∀n:nat. n ≤ f n.
-#f #incr #n (elim n) /2/
-qed.
-
-theorem increasing_to_le: ∀f:nat → nat.
- increasing f → ∀m:nat.∃i.m ≤ f i.
-#f #incr #m (elim m) /2/#n * #a #lenfa
-@(ex_intro ?? (S a)) /2/
-qed.
-
-theorem increasing_to_le2: ∀f:nat → nat. increasing f →
- ∀m:nat. f 0 ≤ m → ∃i. f i ≤ m ∧ m < f (S i).
-#f #incr #m #lem (elim lem)
- [@(ex_intro ? ? O) /2/
- |#n #len * #a * #len #ltnr (cases(le_to_or_lt_eq … ltnr)) #H
- [@(ex_intro ? ? a) % /2/
- |@(ex_intro ? ? (S a)) % //
- ]
- ]
-qed.
-
-theorem increasing_to_injective: ∀f:nat → nat.
- increasing f → injective nat nat f.
-#f #incr #n #m cases(decidable_le n m)
- [#lenm cases(le_to_or_lt_eq … lenm) //
- #lenm #eqf @False_ind @(absurd … eqf) @lt_to_not_eq
- @increasing_to_monotonic //
- |#nlenm #eqf @False_ind @(absurd … eqf) @sym_not_eq
- @lt_to_not_eq @increasing_to_monotonic /2/
- ]
-qed.
-
-(*********************** monotonicity ***************************)