BT0039

gauss_coprime_cancel

Stable · empty-context checked

Cancel a coprime factor from a divisibility witness (Gauss cancellation).

Exact expanded PA statement

forall a b z. (forall d. (exists x. a = d * x) -> (exists y. b = d * y) -> d = 1) -> (exists q. b * z = a * q) -> exists w. z = a * w

Structural proof guide

Cancel a coprime factor from a divisibility witness (Gauss cancellation).

Direct prerequisites: multiple_refl, one_mul, coprime_balanced_bezout, balanced_combination_scale_right, common_divisor_divides_balanced_result. The authored body proceeds by case analysis (4), intermediate claims (2), equality transport (1).

Proof neighborhood

Direct dependencies

BT0028 multiple_refl BT0009 one_mul BT0038 coprime_balanced_bezout BT0036 balanced_combination_scale_right BT0037 common_divisor_divides_balanced_result

Direct dependents

BT003N euclid_prime_dvd_product BT004K beta_moduli_coprime_of_gap_dvd BT004R coprime_mul_left BT00BG coprime_product_is_lcm

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 z
  4. 0004intro hcop
  5. 0005intro hdiv
  6. 0006have hbez : exists xp yp xn yn. a * xp + b * yp = 1 + (a * xn + b * yn)
  7. 0007apply coprime_balanced_bezout
  8. 0008exact hcop
  9. 0009cases hbez
  10. 0010cases hbez_witness
  11. 0011cases hbez_witness_witness
  12. 0012cases hbez_witness_witness_witness
  13. 0013have hscaled : a * (x * z) + (b * z) * x1 = 1 * z + (a * (x2 * z) + (b * z) * x3)
  14. 0014apply balanced_combination_scale_right
  15. 0015exact hbez_witness_witness_witness_witness
  16. 0016specialize one_mul z
  17. 0017rewrite one_mul at hscaled
  18. 0018specialize common_divisor_divides_balanced_result a
  19. 0019specialize common_divisor_divides_balanced_result a
  20. 0020specialize common_divisor_divides_balanced_result (b * z)
  21. 0021specialize common_divisor_divides_balanced_result z
  22. 0022specialize common_divisor_divides_balanced_result (x * z)
  23. 0023specialize common_divisor_divides_balanced_result x1
  24. 0024specialize common_divisor_divides_balanced_result (x2 * z)
  25. 0025specialize common_divisor_divides_balanced_result x3
  26. 0026apply common_divisor_divides_balanced_result
  27. 0027specialize multiple_refl a
  28. 0028exact multiple_refl
  29. 0029exact hdiv
  30. 0030exact hscaled