have : ¬ 3 ∣ 2 := Nat.not_dvd_of_pos_of_lt (by simp) (by simp)
case right
m n q p : ℕ
h : ↑(m • Nat.factorization 2 + n • Nat.factorization 3) 3 = ↑(p • Nat.factorization 2 + q • Nat.factorization 3) 3
⊢ n = q
case right
m n q p : ℕ
h : ↑(m • Nat.factorization 2 + n • Nat.factorization 3) 3 = ↑(p • Nat.factorization 2 + q • Nat.factorization 3) 3
this : ¬3 ∣ 2
⊢ n = q