PA003C

remainder_decomposition_to_mod_eq

Stable checked-use theorem · independently closed

A directed quotient/remainder equation gives balanced congruence to its remainder.

Exact expanded PA statement

forall m b q x. b = q * m + x -> exists u v. b + m * u = x + m * v

Structural proof guide

Generated structural guide

A directed quotient/remainder equation gives balanced congruence to its remainder.

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

The proof proceeds by equality transport (2).

Referenced ingredients

PA000F add_comm PA000H mul_comm

Proof neighborhood

Direct dependencies

PA000F add_comm PA000H mul_comm

Direct dependents

PA005J mod_eq_decidable_from_remainders PA005R quadratic_residue_bounded_equiv PA0063 prime_bounded_nonzero_mod_inverse PA0070 gauss_pointwise_signed_half_representative PA0086 nondivisor_canonical_remainder_exists PA008B prime_mul_index_map_exists_up_to PA008Q prime_scaled_inverse_exists PA00C5 canonical_remainder_from_mod

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 m
  2. 0002intro b
  3. 0003intro q
  4. 0004intro x
  5. 0005intro h
  6. 0006exists 0
  7. 0007exists q
  8. 0008rewrite PA5
  9. 0009rewrite PA3
  10. 0010trans q * m + x
  11. 0011exact h
  12. 0012trans x + q * m
  13. 0013apply add_comm
  14. 0014congr
  15. 0015refl
  16. 0016apply mul_comm