PA001H — is_gcd_euclid

Exact expanded PA statement

forall d a b q r. a = b * q + r -> (((exists x. b = d * x) /\ (exists y. r = d * y)) /\ forall c. (exists u. b = c * u) -> (exists v. r = c * v) -> exists w. d = c * w) -> (((exists x. a = d * x) /\ (exists y. b = d * y)) /\ forall c. (exists u. a = c * u) -> (exists v. b = c * v) -> exists w. d = c * w)

Structural proof guide

Generated structural guide

A relational gcd of divisor and remainder is a gcd of dividend and divisor.

Use the direct prerequisites divides_remainder, divides_linear_step as previously established PA formulas.

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

Referenced ingredients

PA0014 divides_remainder PA001G divides_linear_step

Proof neighborhood

Direct dependencies

PA0014 divides_remainder PA001G divides_linear_step

Direct dependents

PA001K gcd_balanced_bezout_exists_up_to PA0035 gcd_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.