no goals
α : Type u_1
𝕜 : Type u_2
inst✝¹ : Fintype α
inst✝ : LinearOrderedField 𝕜
G H : SimpleGraph α
ε δ : 𝕜
n : ℕ
s : Finset α
hε : FarFromTriangleFree G ε
h : δ ≤ ε
⊢ δ * ↑(Fintype.card α ^ 2) ≤ ε * ↑(Fintype.card α ^ 2)
gcongr