BT004D

bezout_mod_right

Stable · empty-context checked

A balanced Bezout identity selects the left coefficient modulo the right modulus.

Exact expanded PA statement

forall m n xp yp xn yn. m * xp + n * yp = 1 + (m * xn + n * yn) -> exists u v. m * xp + n * u = (1 + m * xn) + n * v

Structural proof guide

A balanced Bezout identity selects the left coefficient modulo the right modulus.

Direct prerequisites: add_assoc. The authored body proceeds by direct introduction and elimination.

Proof neighborhood

Direct dependencies

BT0003 add_assoc

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 m
  2. 0002intro n
  3. 0003intro xp
  4. 0004intro yp
  5. 0005intro xn
  6. 0006intro yn
  7. 0007intro h
  8. 0008exists yp
  9. 0009exists yn
  10. 0010trans 1 + (m * xn + n * yn)
  11. 0011exact h
  12. 0012symm
  13. 0013apply add_assoc