no goals
m n : Nat
⊢ gcd m n ∣ m ∧ gcd m n ∣ n
induction m, n using gcd.induction with
| H0 n => rw [gcd_zero_left]; exact ⟨Nat.dvd_zero n, Nat.dvd_refl n⟩
| H1 m n _ IH => rw [← gcd_rec] at IH; exact ⟨IH.2, (dvd_mod_iff IH.2).1 IH.1⟩
case H0
n : Nat
⊢ n ∣ 0 ∧ n ∣ n
case H0
n : Nat
⊢ gcd 0 n ∣ 0 ∧ gcd 0 n ∣ n
rw [gcd_zero_left]
no goals
case H0
n : Nat
⊢ n ∣ 0 ∧ n ∣ n
exact ⟨Nat.dvd_zero n, Nat.dvd_refl n⟩
case H1
m n : Nat
a✝ : 0 < m
IH : gcd m n ∣ n % m ∧ gcd m n ∣ m
⊢ gcd m n ∣ m ∧ gcd m n ∣ n
case H1
m n : Nat
a✝ : 0 < m
IH : gcd (n % m) m ∣ n % m ∧ gcd (n % m) m ∣ m
⊢ gcd m n ∣ m ∧ gcd m n ∣ n
rw [← gcd_rec] at IH
no goals
case H1
m n : Nat
a✝ : 0 < m
IH : gcd m n ∣ n % m ∧ gcd m n ∣ m
⊢ gcd m n ∣ m ∧ gcd m n ∣ n
exact ⟨IH.2, (dvd_mod_iff IH.2).1 IH.1⟩