PA001W

bezout_mod_left

Stable checked-use theorem · independently closed

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

Exact expanded PA statement

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

Structural proof guide

Generated structural guide

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

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

The proof proceeds by direct introduction and elimination.

Referenced ingredients

PA0009 add_assoc PA000F add_comm

Proof neighborhood

Direct dependencies

PA0009 add_assoc PA000F add_comm

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 xp
  9. 0009exists xn
  10. 0010trans m * xp + n * yp
  11. 0011apply add_comm
  12. 0012trans 1 + (m * xn + n * yn)
  13. 0013exact h
  14. 0014trans 1 + (n * yn + m * xn)
  15. 0015congr
  16. 0016refl
  17. 0017apply add_comm
  18. 0018symm
  19. 0019apply add_assoc