PA0025

mod_eq_predecessor_cancel

Stable checked-use theorem · independently closed

The predecessor of a successor acts as minus one in balanced congruence.

Exact expanded PA statement

forall k a z. exists u v. ((a + z) + k * z) + S k * u = a + S k * v

Structural proof guide

Generated structural guide

The predecessor of a successor acts as minus one in balanced congruence.

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

The proof proceeds by equality transport (3).

Referenced ingredients

PA0009 add_assoc PA000F add_comm PA000G mul_succ_left

Proof neighborhood

Direct dependencies

PA0009 add_assoc PA000F add_comm PA000G mul_succ_left

Direct dependents

PA0026 binary_crt PA003Q coprime_mod_inverse

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 k
  2. 0002intro a
  3. 0003intro z
  4. 0004exists 0
  5. 0005exists z
  6. 0006rewrite PA5
  7. 0007rewrite PA3
  8. 0008specialize mul_succ_left k
  9. 0009specialize mul_succ_left z
  10. 0010rewrite mul_succ_left
  11. 0011trans a + (z + k * z)
  12. 0012apply add_assoc
  13. 0013congr
  14. 0014refl
  15. 0015apply add_comm