Recurrence 2 lookup certificate: exceptional coefficient lookup

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

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Exceptional_coeff_0 : Polynomial.coeff exceptional2 0 = 0

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Exceptional_coeff_1 : Polynomial.coeff exceptional2 1 = 0

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Exceptional_coeff_2 : Polynomial.coeff exceptional2 2 = -1

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Exceptional_coeff_3 : Polynomial.coeff exceptional2 3 = 1

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Exceptional_natDegree_le : Polynomial.natDegree exceptional2 ≤ 3

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Exceptional_coeff_high (n : ℕ) (h : 3 < n) : Polynomial.coeff exceptional2 n = 0