neg_neg

Énoncé

∀ (a : ℝ), - -a = a

L’opposé de l’opposé redonne le nombre. Première démonstration qui en réutilise une autre.

Axiomes consommés

Cet énoncé dépend de 4 axiomes, et d’aucun autre. La liste est relevée par le noyau lui-même (#print axioms), pas déclarée à la main.

• ax1_add_comm
• ax3_add_assoc
• ax4_add_zero
• ax5_add_neg

Vocabulaire admis : myAdd, myNeg, 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 2.** Involutivité de l'opposé.

Choisi délibérément (SPEC.md §5.5) : il exerce `calc`, `Eq.symm` et `congrArg` avec un motif,
et surtout **il réutilise `zero_add`**. C'est exactement la boucle que le produit doit rendre
possible à la souris — démontrer, promouvoir, réemployer. -/
theorem neg_neg : ∀ a : ℝ, -(-a) = a :=
  fun a =>
    Eq.symm
      (calc a
          = a + 0                    := Eq.symm (ax4_add_zero a)
        _ = a + ((-a) + (-(-a)))     := congrArg (fun x => a + x) (Eq.symm (ax5_add_neg (-a)))
        _ = (a + (-a)) + (-(-a))     := Eq.symm (ax3_add_assoc a (-a) (-(-a)))
        _ = 0 + (-(-a))              := congrArg (fun x => x + (-(-a))) (ax5_add_neg a)
        _ = -(-a)                    := zero_add (-(-a)))