no goals
m n k : Nat
⊢ gcd (m * n) (m * k) = m * gcd n k
induction n, k using gcd.induction with
| H0 k => simp
| H1 n k _ IH => rwa [← mul_mod_mul_left, ← gcd_rec, ← gcd_rec] at IH
no goals
case H0
m k : Nat
⊢ gcd (m * 0) (m * k) = m * gcd 0 k
simp
no goals
case H1
m n k : Nat
a✝ : 0 < n
IH : gcd (m * (k % n)) (m * n) = m * gcd (k % n) n
⊢ gcd (m * n) (m * k) = m * gcd n k
rwa [← mul_mod_mul_left, ← gcd_rec, ← gcd_rec] at IH