intro B hB
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
A : Finset α
t : ℕ
v : α
hA : ∀ (B : Finset α), B ⊆ A → ¬IsNClique G (t + 2) B
hv : v ∈ A
⊢ ∀ (B : Finset α), B ⊆ nbhdRes G v A → ¬IsNClique G (t + 1) B
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
A : Finset α
t : ℕ
v : α
hA : ∀ (B : Finset α), B ⊆ A → ¬IsNClique G (t + 2) B
hv : v ∈ A
B : Finset α
hB : B ⊆ nbhdRes G v A
⊢ ¬IsNClique G (t + 1) B