PA00D1

mod_eq_add_cancel_left

Alpha v34 checked-use theorem · independently closed; not Stable

Balanced congruence cancels a common additive left term constructively.

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 d a b c. (exists fspm_u_cancel_input fspm_v_cancel_input. (a + b) + d * fspm_u_cancel_input = (a + c) + d * fspm_v_cancel_input) -> (exists fspm_u_cancel_result fspm_v_cancel_result. (b) + d * fspm_u_cancel_result = (c) + d * fspm_v_cancel_result)

Structural proof guide

Generated structural guide

Balanced congruence cancels a common additive left term constructively.

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

The proof proceeds by case analysis (2).

Referenced ingredients

PA002B add_left_cancel PA0009 add_assoc

Proof neighborhood

Direct dependencies

PA002B add_left_cancel PA0009 add_assoc

Direct dependents

PA00D2 mod_two_cancel_middle

Formal native tactic body

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

Read the argument

Proof checkpoints

19 script commands · 8 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 left canceladd assoc
01Fix variables and assumptionsL1–5

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

  1. L1
    intro d
  2. L2
    intro a
  3. L3
    intro b
  4. L4
    intro c
  5. L5
    intro hmod
02Separate the logical casesL6–7

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L6
    cases hmod
  2. L7
    cases hmod_witness
03Construct an explicit witnessL8–9

Supply the displayed value, then prove that it has the required property.

  1. L8
    exists x
  2. L9
    exists x1
04Use earlier factsL10–13

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

  1. L10
    specialize add_left_cancel a
  2. L11
    specialize add_left_cancel (b + d * x)
  3. L12
    specialize add_left_cancel (c + d * x1)
  4. L13
    apply add_left_cancel
05Calculate and transport equalitiesL14–15

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

  1. L14
    trans (a + b) + d * x
  2. L15
    symm
06Use earlier factsL16–16

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

  1. L16
    apply add_assoc
07Calculate and transport equalitiesL17–17

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

  1. L17
    trans (a + c) + d * x1
08Use earlier factsL18–19

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

  1. L18
    exact hmod_witness_witness
  2. L19
    apply add_assoc

Library-wide reading audit

Original exact command ledger · 19 lines
  1. 0001intro d
  2. 0002intro a
  3. 0003intro b
  4. 0004intro c
  5. 0005intro hmod
  6. 0006cases hmod
  7. 0007cases hmod_witness
  8. 0008exists x
  9. 0009exists x1
  10. 0010specialize add_left_cancel a
  11. 0011specialize add_left_cancel (b + d * x)
  12. 0012specialize add_left_cancel (c + d * x1)
  13. 0013apply add_left_cancel
  14. 0014trans (a + b) + d * x
  15. 0015symm
  16. 0016apply add_assoc
  17. 0017trans (a + c) + d * x1
  18. 0018exact hmod_witness_witness
  19. 0019apply add_assoc