Recurrence 2 lookup certificate: scalar residual identity 1

This is a checked coefficient-lookup shard for the second pseudo-division recurrence in the order-seven certificate.

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.scalarResidual2Coefficient1 : remainder3Coefficient5 ^ 2 * remainder2Coefficient1 = remainder3Coefficient0 * (remainder3Coefficient5 * remainder2Coefficient6) + remainder3Coefficient1 * (remainder3Coefficient5 * remainder2Coefficient5 - remainder3Coefficient4 * remainder2Coefficient6) + remainder2Coefficient6 ^ 2 * exceptional2 * remainder4Coefficient1