Théorèmes sur les entiers naturels (type nat)

Pour avoir accès aux théorèmes avec leurs noms courts :
Require Import PeanoNat.
Import Nat.

Addition
add_0_l : ∀ n : nat, 0 + n = n
add_0_r : ∀ n : nat, n + 0 = n
add_1_l : ∀ n : nat, 1 + n = S n
add_1_r : ∀ n : nat, n + 1 = S n
add_succ_l : ∀ n m : nat, S n + m = S (n + m)
add_succ_r : ∀ n m : nat, n + S m = S (n + m)
add_assoc : ∀ n m p : nat, n + (m + p) = n + m + p
add_comm : ∀ n m : nat, n + m = m + n
eq_add_0 : ∀ n m : nat, n + m = 0 ↔ n = 0 ∧ m = 0
eq_add_1 : ∀ n m : nat, n + m = 1 → n = 1 ∧ m = 0 ∨ n = 0 ∧ m = 1
add_sub : ∀ n m : nat, n + m - m = n
add_sub_eq_l : ∀ n m p : nat, m + p = n → n - m = p
add_sub_eq_r : ∀ n m p : nat, m + p = n → n - p = m

Multiplication
mul_0_l : ∀ n : nat, 0 * n = 0
mul_0_r : ∀ n : nat, n * 0 = 0
mul_1_l : ∀ n : nat, 1 * n = n
mul_1_r : ∀ n : nat, n * 1 = n
mul_assoc : ∀ n m p : nat, n * (m * p) = n * m * p
mul_comm : ∀ n m : nat, n * m = m * n
mul_id_l : ∀ n m : nat, m ≠ 0 → n * m = m ↔ n = 1
mul_id_r : ∀ n m : nat, n ≠ 0 → n * m = n ↔ m = 1
mul_add_distr_l : ∀ n m p : nat, n * (m + p) = n * m + n * p
mul_add_distr_r : ∀ n m p : nat, (n + m) * p = n * p + m * p
mul_sub_distr_l : ∀ n m p : nat, p * (n - m) = p * n - p * m
mul_sub_distr_r : ∀ n m p : nat, (n - m) * p = n * p - m * p

Ordres, min, max
le_trans : ∀ n m p : nat, n ≤ m → m ≤ p → n ≤ p
le_refl : ∀ n : nat, n ≤ n
le_antisymm : ∀ n m : nat, n ≤ m → m ≤ n → n = m
le_succ_r : ∀ n m : nat, n ≤ S m ↔ n ≤ m ∨ n = S m
le_gt_cases : ∀ n m : nat, n ≤ m ∨ m < n
max_l : ∀ n m : nat, m ≤ n → max n m = n
max_r : ∀ n m : nat, n ≤ m → max n m = m
le_max_l : ∀ n m : nat, n ≤ max n m
le_max_r : ∀ n m : nat, m ≤ max n m
max_lub_l : ∀ n m p : nat, max n m ≤ p → n ≤ p
max_lub_r : ∀ n m p : nat, max n m ≤ p → m ≤ p