Theorem: associated_gcd_gcd (NazgandLean4/IntegerInduction.lean)

State before:
a b : ℤ
⊢ Associated (IsBezout.gcd a b) (GCDMonoid.gcd a b)
Tactic:
exact IsBezout.associated_gcd_gcd ℤ
State after:
no goals