Exercices supplémentaires sur les entiers naturels

Pour résoudre ces exercices, vous pouvez utiliser les théorèmes suivants (déjà prouvés dans Naturels) :

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_comm : ∀ n m : nat, n + m = m + n
add_assoc : ∀ n m p : nat, n + (m + p) = (n + m) + p
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_succ_l : ∀ n m : nat, S n * m = n * m + m
mul_succ_r : ∀ n m : nat, n * S m = n * m + n
mul_comm : ∀ n m : nat, n * m = m * n ainsi, bien sûr, que les théorèmes prouvés précédemment dans ce sujet.

Pour vous souvenir de l'énoncé, vous pouvez utiliser la commande Check.

Indice pour le sens direct : faire une preuve par cas sur la nullité ou non de n ou de m (utiliser la tactique destruct).

Utiliser rewrite et les théorèmes précédents.