Require Export Arith.
Require Export Compare.

Lemma not_S_eq : ∀ n m : nat, S n ≠ S m → n ≠ m.
auto with arith.
Qed.
Hint Immediate not_S_eq.

Lemma neq_O_le : ∀ n : nat, n ≠ 0 → 1 ≤ n.
simple induction n; auto with arith.
Qed.
Hint Immediate neq_O_le.

Lemma lt_O : ∀ m n : nat, m < n → 0 < n.
intros m n H.
apply le_lt_trans with m; auto with arith.
Qed.
Hint Immediate lt_O.

Lemma lt_Ex_n : ∀ n : nat, 0 < n → ∃ n0 : nat, n = S n0.
intros.
elim H.
∃ 0; try trivial.
intros; ∃ m; try trivial.
Qed.
Hint Immediate lt_Ex_n.

Lemma lt_m_neq : ∀ m n : nat, m < n → n ≠ m.
simple induction m.
simple induction n; auto with arith.
clear m; intros m H_rec n H.
cut (∃ p : nat, n = S p).
intros G; elim G; clear G.
intros p e.
rewrite e.
apply not_eq_S.
apply H_rec.
apply lt_S_n.
elim e; try trivial.
apply lt_Ex_n.
apply lt_O with (S m); try trivial.
Qed.
Hint Immediate lt_m_neq.