m n : ℕ+
⊢ gcd m n = 1 → gcd n m = 1
m n : ℕ+
⊢ Coprime m n → Coprime n m
unfold Coprime
m n : ℕ+
⊢ gcd n m = 1 → gcd n m = 1
m n : ℕ+
⊢ gcd m n = 1 → gcd n m = 1
rw [gcd_comm]
no goals
m n : ℕ+
⊢ gcd n m = 1 → gcd n m = 1
simp