Half Binomial Coeff pair abs signed

import Mathlib.Algebra.BigOperators.NatAntidiagonal
import Mathlib.Analysis.Complex.Basic
import Mathlib.Analysis.Normed.Ring.Basic
import Mathlib.Analysis.SpecificLimits.Normed
import Mathlib.Data.Sym.Basic
import Mathlib.Data.Sym.Card
import Mathlib.RingTheory.Binomial
import Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
import Definitions.Def_D1Bound5_HalfBinomialCoefficients_Definitions

section
open Finset

namespace D1Bound5






theorem _root_.D1Bound5.halfBinomialCoeff_pair_abs_signed (i j : ℕ) :
    |halfBinomialCoeff (i + 1) * halfBinomialCoeff (j + 1)| =
       (-1 : ℝ) ^ (i + j + 2) *
         (halfBinomialCoeff (i + 1) * halfBinomialCoeff (j + 1)) := by sorry





end D1Bound5
end