PA0068

antisymm_from_witnesses

Stable checked-use theorem · independently closed

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

Generated structural guide

Opposing additive witnesses force equality.

Use the direct prerequisites add_assoc, drop_add_prefix_from_fixed as previously established PA formulas.

The proof proceeds by equality transport (4).

Referenced ingredients

PA0009 add_assoc PA0067 drop_add_prefix_from_fixed

Proof neighborhood

Direct dependencies

PA0009 add_assoc PA0067 drop_add_prefix_from_fixed

Direct dependents

PA0069 le_antisymm

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Linked names are exact direct references. This Stable checked-use theorem is independently kernel-checked when replayed.

  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