Exact expanded PA statement
forall a b. (forall d. (exists x. a = d * x) -> (exists y. b = d * y) -> d = 1) -> forall c. (exists u. b = c * u) -> (exists v. a = c * v) -> c = 1Structural proof guide
Coprimality in its expanded common-divisor form is symmetric.
Direct prerequisites: none. The authored body proceeds by direct introduction and elimination.
Proof neighborhood
Direct dependencies
none
Direct dependents
Formal native tactic body
Dependencies are hypotheses of this body receipt. The focused endpoint audits separately check the complete empty-context certificates.