BT0033

balanced_bezout_euclid_step

Stable · empty-context checked

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

Transport balanced natural Bezout coefficients across one Euclidean division step.

Direct prerequisites: add_assoc, add_comm, mul_add, mul_assoc, add_mul, add_permute_outer. The authored body proceeds by equality transport (1).

Proof neighborhood

Direct dependencies

BT0003 add_assoc BT0002 add_comm BT0007 mul_add BT0008 mul_assoc BT000B add_mul BT0032 add_permute_outer

Direct dependents

BT0034 gcd_balanced_bezout_exists_up_to

Formal native tactic body

Dependencies are hypotheses of this body receipt. The focused endpoint audits separately check the complete empty-context certificates.

  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