Mutate roots

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

section
namespace D1Bound5




theorem _root_.D1Bound5.mutate_roots {R : Type*} [CommRing R] (a b z r0 r s : R)
    (h0 : r0^2 = a*b+1) (hr : r^2 = a*z+1) (hs : s^2 = b*z+1) :
    (r0*r+a*s)^2 = a*mutate a b z r0 r s+1 ∧
    (b*r+r0*s)^2 = b*mutate a b z r0 r s+1 := by sorry





end D1Bound5
end