BT004E

mod_eq_predecessor_cancel

Stable · empty-context checked

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

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

Direct prerequisites: add_assoc, add_comm, mul_succ_left. The authored body proceeds by equality transport (3).

Proof neighborhood

Direct dependencies

BT0003 add_assoc BT0002 add_comm BT0005 mul_succ_left

Direct dependents

BT004F binary_crt

Formal native tactic body

Dependencies are hypotheses of this body receipt. The focused endpoint audits separately check the complete empty-context certificates.

  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