rw [isNClique_iff, coe_insert, coe_singleton, isClique_iff, Set.pairwise_pair_of_symmetric G.symm]
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
a b : α
h : Adj G a b
⊢ IsNClique G 2 {a, b}
α : 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