PA00D1

mod_eq_add_cancel_left

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

Balanced congruence cancels a common additive left term constructively.

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-v16 checked-use theorem is independently kernel-checked when replayed; it is not a Stable theorem.

  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