rcases hf with (hdvd3 | hdvd2)
hwo : (∀ (a b c : ℕplus), (a ∣ b → b ∣ c → a ∣ c) ∧ (a ∣ b → b ∣ a → a = b)) ∧ ∀ (a b : ℕplus), a ∣ b ∨ b ∣ a
hf : 2 ∣ 3 ∨ 3 ∣ 2
⊢ False
case inl
hwo : (∀ (a b c : ℕplus), (a ∣ b → b ∣ c → a ∣ c) ∧ (a ∣ b → b ∣ a → a = b)) ∧ ∀ (a b : ℕplus), a ∣ b ∨ b ∣ a
hdvd3 : 2 ∣ 3
⊢ False

case inr
hwo : (∀ (a b c : ℕplus), (a ∣ b → b ∣ c → a ∣ c) ∧ (a ∣ b → b ∣ a → a = b)) ∧ ∀ (a b : ℕplus), a ∣ b ∨ b ∣ a
hdvd2 : 3 ∣ 2
⊢ False