Recurrence 1 certificate: NormalizedInner2

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.recurrence1NormalizedInner2 : recurrence1Remainder26 ^ 2 * recurrence1Source2 = recurrence1Remainder21 * recurrence1Remainder26 + recurrence1Remainder22 * recurrence1QuotientConstant + recurrence1Exceptional * recurrence1Remainder32