rw [Subtype.ext_iff] at hc
case inl.intro
hwo : (∀ (a b c : ℕplus), (a ∣ b → b ∣ c → a ∣ c) ∧ (a ∣ b → b ∣ a → a = b)) ∧ ∀ (a b : ℕplus), a ∣ b ∨ b ∣ a
c : ℕplus
hc : 3 = 2 * c
⊢ False
case inl.intro
hwo : (∀ (a b c : ℕplus), (a ∣ b → b ∣ c → a ∣ c) ∧ (a ∣ b → b ∣ a → a = b)) ∧ ∀ (a b : ℕplus), a ∣ b ∨ b ∣ a
c : ℕplus
hc : ↑3 = ↑(2 * c)
⊢ False