no goals
k m n : Nat
⊢ k ∣ m → k ∣ n → k ∣ gcd m n
induction m, n using gcd.induction with intro km kn
| H0 n => rw [gcd_zero_left]; exact kn
| H1 n m _ IH => rw [gcd_rec]; exact IH ((dvd_mod_iff km).2 kn) km
case H0
k n : Nat
km : k ∣ 0
kn : k ∣ n
⊢ k ∣ n
case H0
k n : Nat
km : k ∣ 0
kn : k ∣ n
⊢ k ∣ gcd 0 n
rw [gcd_zero_left]
no goals
case H0
k n : Nat
km : k ∣ 0
kn : k ∣ n
⊢ k ∣ n
exact kn
case H1
k n m : Nat
a✝ : 0 < n
IH : k ∣ m % n → k ∣ n → k ∣ gcd (m % n) n
km : k ∣ n
kn : k ∣ m
⊢ k ∣ gcd (m % n) n
case H1
k n m : Nat
a✝ : 0 < n
IH : k ∣ m % n → k ∣ n → k ∣ gcd (m % n) n
km : k ∣ n
kn : k ∣ m
⊢ k ∣ gcd n m
rw [gcd_rec]
no goals
case H1
k n m : Nat
a✝ : 0 < n
IH : k ∣ m % n → k ∣ n → k ∣ gcd (m % n) n
km : k ∣ n
kn : k ∣ m
⊢ k ∣ gcd (m % n) n
exact IH ((dvd_mod_iff km).2 kn) km