Extension product

import Mathlib.Algebra.Ring.Basic
import Mathlib.Algebra.Ring.Equiv
import Mathlib.Data.Finset.Card
import Mathlib.Tactic.Ring
import Definitions.Def_D1Bound5_Regular_Definitions

section
namespace D1Bound5








theorem _root_.D1Bound5.extension_product {R : Type*} [CommRing R] (a b c r s t : R)
    (hr : r ^ 2 = a*b+1) (hs : s ^ 2 = a*c+1) (ht : t ^ 2 = b*c+1) :
    (a+b+c+2*a*b*c+2*r*s*t) * (a+b+c+2*a*b*c-2*r*s*t) =
      regularDefect a b c := by sorry



end D1Bound5
end