PA001P

gauss_coprime_cancel

Stable checked-use theorem · independently closed

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

Generated structural guide

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

Use the direct prerequisites multiple_refl, one_mul, coprime_balanced_bezout, balanced_combination_scale_right, common_divisor_divides_balanced_result as previously established PA formulas.

The proof proceeds by case analysis (4), intermediate claims (2), equality transport (1).

Referenced ingredients

PA0019 multiple_refl PA000M one_mul PA001M coprime_balanced_bezout PA001N balanced_combination_scale_right PA001O common_divisor_divides_balanced_result

Proof neighborhood

Direct dependencies

PA0019 multiple_refl PA000M one_mul PA001M coprime_balanced_bezout PA001N balanced_combination_scale_right PA001O common_divisor_divides_balanced_result

Direct dependents

PA001Q beta_moduli_coprime_of_gap_dvd PA001T coprime_mul_left PA0038 euclid_prime_dvd_product

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