push_neg
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
s : ℕ
A : Finset α
h : card A < s
B : Finset α
hB : B ⊆ A
⊢ ¬(IsClique G ↑B ∧ card B = s)
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
s : ℕ
A : Finset α
h : card A < s
B : Finset α
hB : B ⊆ A
⊢ IsClique G ↑B → card B ≠ s