BT001X

add_eq_zero_left

Stable · empty-context checked

A sum equal to zero has zero as its left addend.

Exact expanded PA statement

forall a b. a + b = 0 -> a = 0

Structural proof guide

A sum equal to zero has zero as its left addend.

Direct prerequisites: add_comm, add_eq_zero_right. The authored body proceeds by direct introduction and elimination.

Proof neighborhood

Direct dependencies

BT0002 add_comm BT000L add_eq_zero_right

Direct dependents

BT0024 two_large_factors_impossible BT004N bounded_common_multiple_exists BT006N prime_three

Formal native tactic body

Dependencies are hypotheses of this body receipt. The focused endpoint audits separately check the complete empty-context certificates.

  1. 0001intro a
  2. 0002intro b
  3. 0003intro h
  4. 0004specialize add_eq_zero_right b
  5. 0005specialize add_eq_zero_right a
  6. 0006apply add_eq_zero_right
  7. 0007trans a + b
  8. 0008apply add_comm
  9. 0009exact h