Initial resultant recurrence certificates for order-seven branch zero

This internal proof shard checks a balanced subset of the independent coefficient identities used by the initial pseudo-remainder recurrence.

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence0Inner30 : selectionCofactorCoefficient30 = divisionCofactor0Coefficient4 * quotient0Coefficient26 + divisionCofactor0Coefficient5 * quotient0Coefficient25 + divisionCofactor0Coefficient6 * quotient0Coefficient24 + divisionCofactor0Coefficient7 * quotient0Coefficient23

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence0Inner31 : selectionCofactorCoefficient31 = divisionCofactor0Coefficient5 * quotient0Coefficient26 + divisionCofactor0Coefficient6 * quotient0Coefficient25 + divisionCofactor0Coefficient7 * quotient0Coefficient24

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence0Inner32 : selectionCofactorCoefficient32 = divisionCofactor0Coefficient6 * quotient0Coefficient26 + divisionCofactor0Coefficient7 * quotient0Coefficient25

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence0Inner33 : selectionCofactorCoefficient33 = divisionCofactor0Coefficient7 * quotient0Coefficient26