Irregular extensions ne zero

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.irregular_extensions_ne_zero {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) (hi : regularDefect a b c ≠ 0) :
    a+b+c+2*a*b*c+2*r*s*t ≠ 0 ∧ a+b+c+2*a*b*c-2*r*s*t ≠ 0 := by sorry

end D1Bound5
end