BT003W

mod_eq_bounded_unique

Stable · empty-context checked

Two balanced-congruent values below the same modulus are equal.

Exact expanded PA statement

forall m a b. (exists ha. ha + S a = m) -> (exists hb. hb + S b = m) -> (exists u v. a + m * u = b + m * v) -> a = b

Structural proof guide

Two balanced-congruent values below the same modulus are equal.

Direct prerequisites: add_comm, division_remainder_unique. The authored body proceeds by case analysis (3), intermediate claims (3).

Proof neighborhood

Direct dependencies

BT0002 add_comm BT001U division_remainder_unique

Direct dependents

BT003X mod_eq_to_remainder_decomposition

Formal native tactic body

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

  1. 0001intro m
  2. 0002intro a
  3. 0003intro b
  4. 0004intro ha
  5. 0005intro hb
  6. 0006intro hab
  7. 0007cases hab
  8. 0008cases hab_witness
  9. 0009have hda : a + m * x = m * x + a
  10. 0010apply add_comm
  11. 0011have hdb : a + m * x = m * x1 + b
  12. 0012trans b + m * x1
  13. 0013exact hab_witness_witness
  14. 0014apply add_comm
  15. 0015specialize division_remainder_unique m
  16. 0016specialize division_remainder_unique (a + m * x)
  17. 0017specialize division_remainder_unique x
  18. 0018specialize division_remainder_unique a
  19. 0019specialize division_remainder_unique x1
  20. 0020specialize division_remainder_unique b
  21. 0021have huniq : x = x1 /\ a = b
  22. 0022apply division_remainder_unique
  23. 0023exact hda
  24. 0024exact ha
  25. 0025exact hdb
  26. 0026exact hb
  27. 0027cases huniq
  28. 0028exact huniq_right