Recurrence 1 certificate: Inner

This file is a checked bounded-band arithmetic shard for the first pseudo-division recurrence in the order-seven branch-zero resultant certificate.

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence1_inner_0 : remainder2Coefficient6 ^ 2 * divisionCofactor0Coefficient0 = remainder2Coefficient0 * (remainder2Coefficient6 * divisionCofactor0Coefficient6 - remainder2Coefficient5 * divisionCofactor0Coefficient7) + divisionCofactor0Coefficient7 ^ 2 * exceptional1 * remainder3Coefficient0

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence1_inner_1 : remainder2Coefficient6 ^ 2 * divisionCofactor0Coefficient1 = remainder2Coefficient0 * (remainder2Coefficient6 * divisionCofactor0Coefficient7) + remainder2Coefficient1 * (remainder2Coefficient6 * divisionCofactor0Coefficient6 - remainder2Coefficient5 * divisionCofactor0Coefficient7) + divisionCofactor0Coefficient7 ^ 2 * exceptional1 * remainder3Coefficient1

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence1_inner_2 : remainder2Coefficient6 ^ 2 * divisionCofactor0Coefficient2 = remainder2Coefficient1 * (remainder2Coefficient6 * divisionCofactor0Coefficient7) + remainder2Coefficient2 * (remainder2Coefficient6 * divisionCofactor0Coefficient6 - remainder2Coefficient5 * divisionCofactor0Coefficient7) + divisionCofactor0Coefficient7 ^ 2 * exceptional1 * remainder3Coefficient2

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence1_inner_3 : remainder2Coefficient6 ^ 2 * divisionCofactor0Coefficient3 = remainder2Coefficient2 * (remainder2Coefficient6 * divisionCofactor0Coefficient7) + remainder2Coefficient3 * (remainder2Coefficient6 * divisionCofactor0Coefficient6 - remainder2Coefficient5 * divisionCofactor0Coefficient7) + divisionCofactor0Coefficient7 ^ 2 * exceptional1 * remainder3Coefficient3

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence1_inner_4 : remainder2Coefficient6 ^ 2 * divisionCofactor0Coefficient4 = remainder2Coefficient3 * (remainder2Coefficient6 * divisionCofactor0Coefficient7) + remainder2Coefficient4 * (remainder2Coefficient6 * divisionCofactor0Coefficient6 - remainder2Coefficient5 * divisionCofactor0Coefficient7) + divisionCofactor0Coefficient7 ^ 2 * exceptional1 * remainder3Coefficient4

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence1_inner_5 : remainder2Coefficient6 ^ 2 * divisionCofactor0Coefficient5 = remainder2Coefficient4 * (remainder2Coefficient6 * divisionCofactor0Coefficient7) + remainder2Coefficient5 * (remainder2Coefficient6 * divisionCofactor0Coefficient6 - remainder2Coefficient5 * divisionCofactor0Coefficient7) + divisionCofactor0Coefficient7 ^ 2 * exceptional1 * remainder3Coefficient5