BT000I

antisymm_from_witnesses

Stable · empty-context checked

Opposing additive witnesses force equality.

Exact expanded PA statement

forall a b n m. a + n = m -> b + m = n -> n = m

Structural proof guide

Opposing additive witnesses force equality.

Direct prerequisites: add_assoc, drop_add_prefix_from_fixed. The authored body proceeds by equality transport (4).

Proof neighborhood

Direct dependencies

BT0003 add_assoc BT000H drop_add_prefix_from_fixed

Direct dependents

BT000J le_antisymm

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 n
  4. 0004intro m
  5. 0005intro h_anm
  6. 0006intro h_bmn
  7. 0007symm
  8. 0008rewrite <- h_anm
  9. 0009specialize drop_add_prefix_from_fixed a
  10. 0010specialize drop_add_prefix_from_fixed b
  11. 0011specialize drop_add_prefix_from_fixed n
  12. 0012apply drop_add_prefix_from_fixed
  13. 0013specialize add_assoc b
  14. 0014specialize add_assoc a
  15. 0015specialize add_assoc n
  16. 0016rewrite add_assoc
  17. 0017rewrite h_anm
  18. 0018rewrite h_bmn
  19. 0019refl