ax1_add_comm

Énoncé

∀ (a : ℝ) (b : ℝ), a + b = b + a

L’ordre des termes d’une somme n’a pas d’importance.

Axiomes consommés

C’est un axiome : il est admis, pas démontré. Tout ce qui s’appuie dessus en hérite, et c’est précisément ce que cette bibliothèque rend visible.

• ax1_add_comm

Vocabulaire admis : myAdd, ℝ — les déclarations qui nomment ℝ et ses opérations, communes à toute la bibliothèque.

Code

axiom ax1_add_comm : ∀ a b : ℝ, a + b = b + a