Theorem: Int.gcd_val (AlgebraI/Subgroups.lean)

State before:
a b : ℤ
⊢ gcd a b = gcd (b % a) a
Tactic:
rw [← natAbs_euclideanDomain_gcd, EuclideanDomain.gcd_val, natAbs_euclideanDomain_gcd]
State after:
no goals