Unordered pair double count

import Mathlib

namespace Conway99Formal.TriangleBound
end Conway99Formal.TriangleBound

set_option autoImplicit false

/-! Literal graph counts for the universal triangle and prism claim. -/

open Conway99Formal.TriangleBound

open Finset SimpleGraph

variable {V : Type*} [Fintype V] [DecidableEq V]
variable (G : SimpleGraph V) [DecidableRel G.Adj]

theorem Conway99Formal.TriangleBound.unordered_pair_double_count {A : Type*} [Fintype A] [DecidableEq A]
    (s : Finset A) (R : A → A → Prop) [DecidableRel R]
    (hsym : ∀ a b, R a b → R b a) :
    (∑ a ∈ s, (s.filter fun b => a ≠ b ∧ R a b).card) =
      2 * ((s.powersetCard 2).filter fun p =>
        ∃ a b, a ∈ p ∧ b ∈ p ∧ a ≠ b ∧ R a b).card := by sorry