exact G.clique_free_card_lt h
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
s : ℕ
h✝ : 0 < s
h : card ∅ < s
⊢ CliqueFreeSet ∅ s

α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
s : ℕ
h : 0 < s
⊢ Type ?u.2299
no goals