PA001P

gauss_coprime_cancel

Stable checked-use theorem · independently closed

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

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.

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.

Read the argument

Proof checkpoints

30 script commands · 5 reading checkpoints · 2 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

Named ingredients (5)
multiple reflone mulcoprime balanced bezoutbalanced combination scale rightcommon divisor divides balanced result
01Fix variables and assumptionsL1–5

Work with arbitrary variables or the premises of the current implication.

  1. L1
    intro a
  2. L2
    intro b
  3. L3
    intro z
  4. L4
    intro hcop
  5. L5
    intro hdiv
02Establish hbezL6–8

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply coprime balanced bezout.

  1. L6
    have hbez : exists xp yp xn yn. a * xp + b * yp = 1 + (a * xn + b * yn)
  2. L7
    apply coprime_balanced_bezout
  3. L8
    exact hcop
03Separate the logical casesL9–12

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L9
    cases hbez
  2. L10
    cases hbez_witness
  3. L11
    cases hbez_witness_witness
  4. L12
    cases hbez_witness_witness_witness
04Establish hscaledL13–22

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply balanced combination scale right.

  1. L13
    have hscaled : a * (x * z) + (b * z) * x1 = 1 * z + (a * (x2 * z) + (b * z) * x3)
  2. L14
    apply balanced_combination_scale_right
  3. L15
    exact hbez_witness_witness_witness_witness
  4. L16
    specialize one_mul z
  5. L17
    rewrite one_mul at hscaled
  6. L18
    specialize common_divisor_divides_balanced_result a
  7. L19
    specialize common_divisor_divides_balanced_result a
  8. L20
    specialize common_divisor_divides_balanced_result (b * z)
  9. L21
    specialize common_divisor_divides_balanced_result z
  10. L22
    specialize common_divisor_divides_balanced_result (x * z)
05Use earlier factsL23–30

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L23
    specialize common_divisor_divides_balanced_result x1
  2. L24
    specialize common_divisor_divides_balanced_result (x2 * z)
  3. L25
    specialize common_divisor_divides_balanced_result x3
  4. L26
    apply common_divisor_divides_balanced_result
  5. L27
    specialize multiple_refl a
  6. L28
    exact multiple_refl
  7. L29
    exact hdiv
  8. L30
    exact hscaled

Library-wide reading audit

Original exact command ledger · 30 lines
  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