PA001X

bezout_mod_right

Stable checked-use theorem · independently closed

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

Generated structural guide

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

Use the direct prerequisites add_assoc as previously established PA formulas.

The proof proceeds by direct introduction and elimination.

Referenced ingredients

PA0009 add_assoc

Proof neighborhood

Direct dependencies

PA0009 add_assoc

Direct dependents

PA0026 binary_crt

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 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