ax5_add_neg
admisDeZero.Axiomes
Énoncé
∀ (a : ℝ), a + -a = 0
Tout réel a un opposé : leur somme est nulle.
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.
Vocabulaire admis : myAdd, myNeg, myZero, ℝ — les déclarations qui nomment ℝ et ses opérations, communes à toute la bibliothèque.
Code
axiom ax5_add_neg : ∀ a : ℝ, a + (-a) = 0
S’appuie sur
Rien : c’est un point de départ.