α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a b : α
⊢ (a == b) = false ↔ ¬(a == b) = true
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a b : α
⊢ (a == b) = false ↔ a ≠ b
rw [ne_eq, ← beq_iff_eq a b]
no goals
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a b : α
⊢ (a == b) = false ↔ ¬(a == b) = true
cases a == b <;> decide