exact ⟨fun _ => h, card_eq_two.2 ⟨a,b,G.ne_of_adj h,rfl⟩⟩
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
a b : α
h : Adj G a b
⊢ (a ≠ b → Adj G a b) ∧ card {a, b} = 2
no goals