Recurrence 2 lookup certificate: scalar residual identity 4

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

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.scalarResidual2Coefficient4 : remainder3Coefficient5 ^ 2 * remainder2Coefficient4 = remainder3Coefficient3 * (remainder3Coefficient5 * remainder2Coefficient6) + remainder3Coefficient4 * (remainder3Coefficient5 * remainder2Coefficient5 - remainder3Coefficient4 * remainder2Coefficient6) + remainder2Coefficient6 ^ 2 * exceptional2 * remainder4Coefficient4