Library hydras.Prelude.Compat815

From Coq Require Import Arith Lia.
Import Nat.

Module Compat815.

  Lemma le_n_0_eq : ∀ n : nat, n ≤ 0 → 0 = n.

  Lemma le_lt_or_eq :
    ∀ n m : nat, n ≤ m → n < m ∨ n = m.

  Lemma lt_n_Sm_le:
      ∀ n m : nat, n < S m → n ≤ m.

  Definition ind_0_1_SS (P : nat → Prop) (H0 : P 0) (H1 : P 1)
  (H2 : ∀ n : nat, P n → P (S (S n))) : ∀ n, P n :=

fix ind_0_1_SS (n : nat) : P n :=
  match n as n0 return (P n0) with
  | 0 ⇒ H0
  | S n0 ⇒
      (fun n1 : nat ⇒
       match n1 as n2 return (P (S n2)) with
       | 0 ⇒ H1
       | S n2 ⇒ (fun n3 : nat ⇒ H2 n3 (ind_0_1_SS n3)) n2
       end) n0
  end.

  Lemma lt_S_n (n m :nat) : S n < S m → n < m.


  Lemma lt_n_S : ∀ n m : nat, n < m → S n < S m.

  Lemma le_lt_n_Sm : ∀ n m : nat, n ≤ m → n < S m.

 Lemma lt_not_le : ∀ n m : nat, n < m → ¬ m ≤ n.

 Lemma le_plus_r : ∀ n m : nat, m ≤ n + m.

Lemma mult_O_le : ∀ n m : nat, m = 0 ∨ n ≤ m × n.

Lemma plus_Snm_nSm
     : ∀ n m : nat, S n + m = n + S m.

Lemma n_SSSn : ∀ n : nat, n ≠ S (S (S n)).

Lemma n_SSn : ∀ n : nat, n ≠ S (S n).

Lemma le_not_lt : ∀ n m : nat, n ≤ m → ¬ m < n.

End Compat815.