zero_add
démontréDeZero.Reference
Énoncé
∀ (a : ℝ), 0 + a = a
Ajouter zéro à gauche ne change rien. Se démontre en deux blocs à partir des axiomes 1 et 4.
Axiomes consommés
Cet énoncé dépend de 2 axiomes, et d’aucun autre. La liste est relevée par le noyau lui-même (#print axioms), pas déclarée à la main.
Vocabulaire admis : myAdd, myZero, ℝ — les déclarations qui nomment ℝ et ses opérations, communes à toute la bibliothèque.
Schéma
La démonstration telle qu’elle a été construite dans l’atelier : chaque bloc est une déclaration, chaque fil une application. Rien n’est modifiable ici.
Code
/-- **Théorème 1.** Neutralité à gauche de zéro. Le plus petit théorème utile du corpus, et celui que l'utilisateur reconstruira à la souris au jalon 4 : deux blocs, un fil. -/ theorem zero_add : ∀ a : ℝ, 0 + a = a := fun a => Eq.trans (ax1_add_comm 0 a) (ax4_add_zero a)