add_right_cancel

Énoncé

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

D’une égalité de deux sommes ayant le même terme à droite, on tire l’égalité des deux autres.

Axiomes consommés

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

• 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 3.** Annulation additive à droite.

Le troisième théorème demandé au SPEC.md §5.5 : celui qui prend une **hypothèse**, donc qui
donnera un bloc avec un port d'entrée de type `Prop` et non `ℝ`. C'est la forme de bloc qui
valide le télescopage du §11.3 — quatre entrées, dont la quatrième est une preuve. -/
theorem add_right_cancel : ∀ a b c : ℝ, a + c = b + c → a = b :=
  fun a b c h =>
    calc a
        = a + 0              := Eq.symm (ax4_add_zero a)
      _ = a + (c + (-c))     := congrArg (fun x => a + x) (Eq.symm (ax5_add_neg c))
      _ = (a + c) + (-c)     := Eq.symm (ax3_add_assoc a c (-c))
      _ = (b + c) + (-c)     := congrArg (fun x => x + (-c)) h
      _ = b + (c + (-c))     := ax3_add_assoc b c (-c)
      _ = b + 0              := congrArg (fun x => b + x) (ax5_add_neg c)
      _ = b                  := ax4_add_zero b