Recurrence 2 lookup certificate: scalar residual identity 2

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

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.scalarResidual2Coefficient2 : remainder3Coefficient5 ^ 2 * remainder2Coefficient2 = remainder3Coefficient1 * (remainder3Coefficient5 * remainder2Coefficient6) + remainder3Coefficient2 * (remainder3Coefficient5 * remainder2Coefficient5 - remainder3Coefficient4 * remainder2Coefficient6) + remainder2Coefficient6 ^ 2 * exceptional2 * remainder4Coefficient2