BT000I

antisymm_from_witnesses

Stable checked-use theorem · independently kernel verified

Opposing additive witnesses force equality.

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.

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 the historical Alpha-v12 body receipt. The complete historical Alpha-v18 proof bundle independently checks every dependency; current Alpha v25 preserves that checked theorem use without changing Stable membership.

Read the argument

Proof checkpoints

19 script commands · 4 reading checkpoints · 0 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

Named ingredients (2)
add assocdrop add prefix from fixed
01Fix variables and assumptionsL1–6

Work with arbitrary variables or the premises of the current implication.

  1. L1
    intro a
  2. L2
    intro b
  3. L3
    intro n
  4. L4
    intro m
  5. L5
    intro h_anm
  6. L6
    intro h_bmn
02Calculate and transport equalitiesL7–8

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L7
    symm
  2. L8
    rewrite <- h_anm
03Use earlier factsL9–15

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L9
    specialize drop_add_prefix_from_fixed a
  2. L10
    specialize drop_add_prefix_from_fixed b
  3. L11
    specialize drop_add_prefix_from_fixed n
  4. L12
    apply drop_add_prefix_from_fixed
  5. L13
    specialize add_assoc b
  6. L14
    specialize add_assoc a
  7. L15
    specialize add_assoc n
04Calculate and transport equalitiesL16–19

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L16
    rewrite add_assoc
  2. L17
    rewrite h_anm
  3. L18
    rewrite h_bmn
  4. L19
    refl

Library-wide reading audit

Original exact command ledger · 19 lines
  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