d m n : Nat
dgt1 : 1 < d
Hm : d ∣ m
Hn : d ∣ n
co : coprime m n
⊢ d ∣ gcd m n
d m n : Nat
dgt1 : 1 < d
Hm : d ∣ m
Hn : d ∣ n
co : coprime m n
⊢ d ∣ 1
rw [← co.gcd_eq_one]
no goals
d m n : Nat
dgt1 : 1 < d
Hm : d ∣ m
Hn : d ∣ n
co : coprime m n
⊢ d ∣ gcd m n
exact dvd_gcd Hm Hn