PA001J

balanced_bezout_euclid_step

Stable checked-use theorem · independently closed

Transport balanced natural Bezout coefficients across one Euclidean division step.

Exact expanded PA statement

forall a b q r d xp yp xn yn. a = b * q + r -> b * xp + r * yp = d + (b * xn + r * yn) -> a * yp + b * (xp + q * yn) = d + (a * yn + b * (xn + q * yp))

Structural proof guide

Generated structural guide

Transport balanced natural Bezout coefficients across one Euclidean division step.

Use the direct prerequisites add_assoc, add_comm, mul_add, mul_assoc, add_mul, add_permute_outer as previously established PA formulas.

The proof proceeds by equality transport (1).

Referenced ingredients

PA0009 add_assoc PA000F add_comm PA000A mul_add PA000B mul_assoc PA0016 add_mul PA001I add_permute_outer

Proof neighborhood

Direct dependencies

PA0009 add_assoc PA000F add_comm PA000A mul_add PA000B mul_assoc PA0016 add_mul PA001I add_permute_outer

Direct dependents

PA001K gcd_balanced_bezout_exists_up_to

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 a
  2. 0002intro b
  3. 0003intro q
  4. 0004intro r
  5. 0005intro d
  6. 0006intro xp
  7. 0007intro yp
  8. 0008intro xn
  9. 0009intro yn
  10. 0010intro hab
  11. 0011intro hbez
  12. 0012rewrite hab
  13. 0013trans ((b * q) * yp + r * yp) + b * (xp + q * yn)
  14. 0014congr
  15. 0015apply add_mul
  16. 0016refl
  17. 0017trans ((b * q) * yp + r * yp) + (b * xp + b * (q * yn))
  18. 0018congr
  19. 0019refl
  20. 0020apply mul_add
  21. 0021trans ((b * q) * yp + r * yp) + (b * xp + (b * q) * yn)
  22. 0022congr
  23. 0023refl
  24. 0024congr
  25. 0025refl
  26. 0026symm
  27. 0027apply mul_assoc
  28. 0028trans (b * xp + r * yp) + ((b * q) * yp + (b * q) * yn)
  29. 0029apply add_permute_outer
  30. 0030trans (b * xp + r * yp) + ((b * q) * yn + (b * q) * yp)
  31. 0031congr
  32. 0032refl
  33. 0033apply add_comm
  34. 0034trans (d + (b * xn + r * yn)) + ((b * q) * yn + (b * q) * yp)
  35. 0035congr
  36. 0036exact hbez
  37. 0037refl
  38. 0038trans d + ((b * xn + r * yn) + ((b * q) * yn + (b * q) * yp))
  39. 0039apply add_assoc
  40. 0040trans d + (((b * q) * yn + r * yn) + (b * xn + (b * q) * yp))
  41. 0041congr
  42. 0042refl
  43. 0043apply add_permute_outer
  44. 0044trans d + ((b * q + r) * yn + (b * xn + (b * q) * yp))
  45. 0045congr
  46. 0046refl
  47. 0047congr
  48. 0048symm
  49. 0049apply add_mul
  50. 0050refl
  51. 0051trans d + ((b * q + r) * yn + (b * xn + b * (q * yp)))
  52. 0052congr
  53. 0053refl
  54. 0054congr
  55. 0055refl
  56. 0056congr
  57. 0057refl
  58. 0058apply mul_assoc
  59. 0059congr
  60. 0060refl
  61. 0061congr
  62. 0062congr
  63. 0063symm
  64. 0064exact hab
  65. 0065refl
  66. 0066symm
  67. 0067apply mul_add