V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
h : IsSRGWith G n k ℓ μ
⊢ IsRegularOfDegree (Gᶜ) (Fintype.card V - 1 - k)
V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
h : IsSRGWith G n k ℓ μ
⊢ IsRegularOfDegree (Gᶜ) (n - k - 1)
rw [← h.card, Nat.sub_sub, add_comm, ← Nat.sub_sub]
no goals
V : Type u
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
n k ℓ μ : ℕ
h : IsSRGWith G n k ℓ μ
⊢ IsRegularOfDegree (Gᶜ) (Fintype.card V - 1 - k)
exact h.regular.compl