Recurrence 2 lookup certificate: Scalar2Main coefficient convolution

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

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_92 : Polynomial.coeff recurrence2Scalar2Main 92 = -((18199647 * 10 ^ 70 + 9691564437142171691696125239365115373811139059804463376399933170342398) * 10 ^ 70 + 7686841192484438693317994324656609006918650836432833677353179453974502)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_93 : Polynomial.coeff recurrence2Scalar2Main 93 = (82615696 * 10 ^ 70 + 2759337552822079221469684719671806127806104994354548930647402116728781) * 10 ^ 70 + 191137042352746015458765530531770295214845317622921123571083611139238

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_94 : Polynomial.coeff recurrence2Scalar2Main 94 = -((359239796 * 10 ^ 70 + 234355682966465998133197703393028160060404700941656738416219659833936) * 10 ^ 70 + 2407292092928797250059813087732670781360034503049792495423218155746129)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_95 : Polynomial.coeff recurrence2Scalar2Main 95 = (1493683769 * 10 ^ 70 + 3484533406279069577579741206654555224046668914555705618037706082486034) * 10 ^ 70 + 7982213458294706215688196310672751675732399954382517189387723795801034

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_96 : Polynomial.coeff recurrence2Scalar2Main 96 = -((5919776961 * 10 ^ 70 + 606568419642561712651758372219849973485632223018111794353112339441951) * 10 ^ 70 + 8596510409596973387975543844970017303939222300847021486558382905893750)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_97 : Polynomial.coeff recurrence2Scalar2Main 97 = (22237094224 * 10 ^ 70 + 6643413798754019802367980241020090645212250943484919101428974474097270) * 10 ^ 70 + 7302947107080052997729296415439982990259911513996536364937164337148359

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_98 : Polynomial.coeff recurrence2Scalar2Main 98 = -((78420477004 * 10 ^ 70 + 3596210200962220119080897357468735780484959508127110479611227575852045) * 10 ^ 70 + 3403100751221773810003060031582700377971631171411976377909898928640363)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_99 : Polynomial.coeff recurrence2Scalar2Main 99 = (255563808746 * 10 ^ 70 + 3434558372972373116783263523777411400427905098123742238685763877228713) * 10 ^ 70 + 5725039038020077026666774159616415494247289360179979110625293583002652

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_100 : Polynomial.coeff recurrence2Scalar2Main 100 = -((748951492261 * 10 ^ 70 + 5881866046815239736271268509325527232415227401814318473533590775912511) * 10 ^ 70 + 7098151357229753829156241018501800864705078013274281894511540493231817)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_101 : Polynomial.coeff recurrence2Scalar2Main 101 = (1867124214056 * 10 ^ 70 + 5329374311645379979280092407901283978763409040626749644405839644087864) * 10 ^ 70 + 6362319819207771221288365004669723187345669251741239717297980827118728

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_102 : Polynomial.coeff recurrence2Scalar2Main 102 = -((3346116819860 * 10 ^ 70 + 8859260512942387535045905239579109258181984878975006313184830763913474) * 10 ^ 70 + 7868913204071340732516782314138398223735376607898268554135581820377848)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_103 : Polynomial.coeff recurrence2Scalar2Main 103 = (1117598439 * 10 ^ 70 + 4317070299997385687168402923841720831226923038447230609658758933130775) * 10 ^ 70 + 134500147066463859554865318542920183127683855142890460296086289001949

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_104 : Polynomial.coeff recurrence2Scalar2Main 104 = (39494165531559 * 10 ^ 70 + 9548899146763257233870542135532689473732200026878399033117810093110202) * 10 ^ 70 + 4722518099981123520820255196383891807618999192595344843257327398640633

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_105 : Polynomial.coeff recurrence2Scalar2Main 105 = -((270491688530121 * 10 ^ 70 + 5872616025072480920526523612649933258600934811767094873032412931244224) * 10 ^ 70 + 4888080866932019747166662312972384785040240276355616795453721494442432)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_106 : Polynomial.coeff recurrence2Scalar2Main 106 = (1411649696493261 * 10 ^ 70 + 3410255702363756000595341274507149075137030325910958344293119742039427) * 10 ^ 70 + 7161117101153837808918590229392870831804933834354640172633901617798742

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_107 : Polynomial.coeff recurrence2Scalar2Main 107 = -((6546801337469017 * 10 ^ 70 + 154767033530170386447716218095508616787891410409038819051153582605367) * 10 ^ 70 + 7986666567664317548283848157066570357356712379017697793654980437178525)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_108 : Polynomial.coeff recurrence2Scalar2Main 108 = (27191515996179012 * 10 ^ 70 + 1471221310986874058531676141163307895669995107815750656084283823000565) * 10 ^ 70 + 7418168600941725724125070883876726370853775417537489572432666069343321

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_109 : Polynomial.coeff recurrence2Scalar2Main 109 = -((96774868001203307 * 10 ^ 70 + 482430287523192862844394920993684798430370641556150476154462696418813) * 10 ^ 70 + 8115706035401408297948310566618692388624493616967739190835119053792239)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_110 : Polynomial.coeff recurrence2Scalar2Main 110 = (268955145239699505 * 10 ^ 70 + 2008246648050308110229155512821596094329557966231525998529517966311228) * 10 ^ 70 + 6136969157999921033937298254883854196577338651848879480179009500995780

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_111 : Polynomial.coeff recurrence2Scalar2Main 111 = -((440481819650571093 * 10 ^ 70 + 801852123060705485155925046938296744473999750302390969932402604901518) * 10 ^ 70 + 676895197395705265503181203903163701904871638869316965069591638861361)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_112 : Polynomial.coeff recurrence2Scalar2Main 112 = -((450944165789034084 * 10 ^ 70 + 4864767141509014624970698455662998929991419366793489796554300343036580) * 10 ^ 70 + 5537520233881208060948604987366779378136939250425751105082591327996695)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_113 : Polynomial.coeff recurrence2Scalar2Main 113 = (5371241629953495991 * 10 ^ 70 + 6619924085245617838153316851603109695944974146751961088949578553605868) * 10 ^ 70 + 8755048458682881356351869508027988266633135702639056624708293211060233

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_114 : Polynomial.coeff recurrence2Scalar2Main 114 = -((8902679344999947390 * 10 ^ 70 + 1481688707325825704657968858068732182814384638203038081925867576077216) * 10 ^ 70 + 1214672445762316135133137940847735086653386720210550931360350283840452)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_115 : Polynomial.coeff recurrence2Scalar2Main 115 = -((83057492718088624027 * 10 ^ 70 + 1224469456490807539603072755227470339882238002210502464079347083467086) * 10 ^ 70 + 468501672835082639224792076277821647644365194455487975734656480869414)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_116 : Polynomial.coeff recurrence2Scalar2Main 116 = (751632929655532352457 * 10 ^ 70 + 9408757279226660078248937144460674279487783046229008998698584693278487) * 10 ^ 70 + 9345285018172635017189012248555804676418697546941332174323229527587206

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_117 : Polynomial.coeff recurrence2Scalar2Main 117 = -((3258213788154652648524 * 10 ^ 70 + 8735858516934370687550653076402400852922423499184984748705680665233335) * 10 ^ 70 + 8711267500179481961109390363326429141214594134771785691780353858167308)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_118 : Polynomial.coeff recurrence2Scalar2Main 118 = (6938439881987786550790 * 10 ^ 70 + 9511376215558298778453462353628743127902001842667705232295465790395770) * 10 ^ 70 + 2336497647853970623603723054122807068530341641504792809863988447294283

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_119 : Polynomial.coeff recurrence2Scalar2Main 119 = (14118191629802404709485 * 10 ^ 70 + 2818492525655951721750167952331123960206708121370188769705525985278500) * 10 ^ 70 + 7596118561058526929951863662964232052945225457159763940665948237861855

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_120 : Polynomial.coeff recurrence2Scalar2Main 120 = -((212723220454337360758802 * 10 ^ 70 + 218320943513971648887311889174598924999610843543852229691593346751796) * 10 ^ 70 + 4915113869267603547472976821455854464962872289211133787665042441818705)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_121 : Polynomial.coeff recurrence2Scalar2Main 121 = (1128025539701975188688926 * 10 ^ 70 + 1343689454047061936179931246679190552818638563834252789794446585915579) * 10 ^ 70 + 1963564068765307130833671752069653794977607861392867434626910978575352

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_122 : Polynomial.coeff recurrence2Scalar2Main 122 = -((3626121252669976166597441 * 10 ^ 70 + 7165836055104681539316240300554836425666750722370011533699488775901259) * 10 ^ 70 + 2572495711213773164685735716518000420757483355339221812995422065367093)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_123 : Polynomial.coeff recurrence2Scalar2Main 123 = (4029658895247337459267054 * 10 ^ 70 + 4528042109609880283284684436247180790079246014607476596784836820157899) * 10 ^ 70 + 3344589853051070704508408448210316292618788411361339374907824145319542

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_124 : Polynomial.coeff recurrence2Scalar2Main 124 = (35298347676045526661943578 * 10 ^ 70 + 115237707488565128298099167049777776028282171822623058602160873416630) * 10 ^ 70 + 2712993776652739108573650097584280055783913247746684087511771017460656

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_125 : Polynomial.coeff recurrence2Scalar2Main 125 = -((280531446873040803418505263 * 10 ^ 70 + 7032244053811903288667939294527263391543846144454235945264776536514840) * 10 ^ 70 + 3940812854925099282846476307403433450845234353656278713816491965497186)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_126 : Polynomial.coeff recurrence2Scalar2Main 126 = (1095838059515918501733284497 * 10 ^ 70 + 7616860868742589908052637769973386918544840369178913739882434154812891) * 10 ^ 70 + 5108145396115325085562634625259528155226399559525872717041474792780522

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_127 : Polynomial.coeff recurrence2Scalar2Main 127 = -((2026646295313540755383663439 * 10 ^ 70 + 7838315264810355558708003598301490358347692138133976029939237050571537) * 10 ^ 70 + 4696335737614551161064963410543454078548811235357643877751765606699238)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_128 : Polynomial.coeff recurrence2Scalar2Main 128 = -((4129123046933622548440349010 * 10 ^ 70 + 380486686628063781717891530966773947415785738039298699476567424762163) * 10 ^ 70 + 9939310780616537215837617467238022497286826763099264954310618139471796)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_129 : Polynomial.coeff recurrence2Scalar2Main 129 = (46335006778369258002019556759 * 10 ^ 70 + 3474679060337488500399968182877429164746108146521257341180416640831759) * 10 ^ 70 + 5952929018413053763721271131837750380541950530707957521344213220556345

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_130 : Polynomial.coeff recurrence2Scalar2Main 130 = -((178863255719968698597248545784 * 10 ^ 70 + 1377533502805185970700040466741890853005400927479721311624046924817523) * 10 ^ 70 + 6821603506825328690750959387712776296925670032197018918954706383465)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_131 : Polynomial.coeff recurrence2Scalar2Main 131 = (386082759235756225885018566067 * 10 ^ 70 + 9580686101873023808950215261288625228260221406850551215995247733573641) * 10 ^ 70 + 9308851007909904083724381029583862277102816045653653093985002157627388

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_132 : Polynomial.coeff recurrence2Scalar2Main 132 = -((352449508920830040632821713840 * 10 ^ 70 + 6273706376037527453703772784798313488969812433516799629161670018063426) * 10 ^ 70 + 1454424907745491161910389349884752117164591923088377960901727105458801)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_133 : Polynomial.coeff recurrence2Scalar2Main 133 = -((643566432246781539191298390337 * 10 ^ 70 + 7497925988981182452966046370799609576072384618842520280281505737019749) * 10 ^ 70 + 152656964539094777864561424683680352830171930134072180387077823807377)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_134 : Polynomial.coeff recurrence2Scalar2Main 134 = (6626277951320958781799249129082 * 10 ^ 70 + 4543427510799771411692756911665002433270050846069981878669020969917958) * 10 ^ 70 + 3454065708060656414784434451030018213867155335534860136215510607943199

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_135 : Polynomial.coeff recurrence2Scalar2Main 135 = -((54485586686939198498952599373763 * 10 ^ 70 + 4743892221971204680797036637326688993412608376049192105883084564903873) * 10 ^ 70 + 1321164189810052878425772215850870483653328069665098682692686987591264)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_136 : Polynomial.coeff recurrence2Scalar2Main 136 = (309526800913479912006433288556406 * 10 ^ 70 + 2149070164569158427399078485287220533259734545966017914468650070681320) * 10 ^ 70 + 3578363202890467207457415991277006293298658260413313345405519843732238

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_137 : Polynomial.coeff recurrence2Scalar2Main 137 = -((945290292108872641528855725439743 * 10 ^ 70 + 3517792967443205374394879029770132466246886673990397481179384073748268) * 10 ^ 70 + 7867898120942625258319968268001546969771443848073428026101649669745737)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_138 : Polynomial.coeff recurrence2Scalar2Main 138 = (169763285114945626836936548594403 * 10 ^ 70 + 8494595245409050059689043492028430930236053000630504976369726520205522) * 10 ^ 70 + 4278258614718078079248126894262991913758035846386372832466465868637687

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_139 : Polynomial.coeff recurrence2Scalar2Main 139 = (10611872884979399698253154130620584 * 10 ^ 70 + 2514437562173748094242686336708879467977422683863621823143543265302542) * 10 ^ 70 + 4882395272159961111158311612415118839197427486874781193442252143672804

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_140 : Polynomial.coeff recurrence2Scalar2Main 140 = -((33089263681457064873817674907662872 * 10 ^ 70 + 5167047414019766326817676650265169620060181711526896428690951686804892) * 10 ^ 70 + 6170003963483933779194391059773851456367326425645627107774888182522243)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_141 : Polynomial.coeff recurrence2Scalar2Main 141 = -((45908209715338228744861295835678066 * 10 ^ 70 + 1656588851499292365714574278045454685435094896506160180134116511304100) * 10 ^ 70 + 1267872703011144589362385735182514557323817475904610981425134455249617)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_142 : Polynomial.coeff recurrence2Scalar2Main 142 = (520210097179915534942563429737774788 * 10 ^ 70 + 9641452217672601266267154607446394467435286761600726813869822807161672) * 10 ^ 70 + 8837861379356949846424946351562692201613271851319223708893341146723118

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_143 : Polynomial.coeff recurrence2Scalar2Main 143 = -((102164427714624774254456583053635711 * 10 ^ 70 + 6401912139696179011782584756738638253591932106669599013025035649615375) * 10 ^ 70 + 7244235024394934623505123985573331324088605730879492449563494433225144)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_144 : Polynomial.coeff recurrence2Scalar2Main 144 = -((11767725587110638819383923378014754622 * 10 ^ 70 + 6277397637188672482828176093706090676562783538384891307068051763518390) * 10 ^ 70 + 7048160132899057158960508224569283378597943136157877226473606341156522)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_145 : Polynomial.coeff recurrence2Scalar2Main 145 = (54278452074130025735485116508205669232 * 10 ^ 70 + 8551368966767638904503348851486129030103114100294561263088985148624948) * 10 ^ 70 + 8354320270625750133492323484115013867872138217639282233257933092384118

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_146 : Polynomial.coeff recurrence2Scalar2Main 146 = -((27173337470222222866710661417093738957 * 10 ^ 70 + 5328971513544227314490238202873040965304990720863674815788212396739409) * 10 ^ 70 + 3375521457013598106196401829518706954572543352761752825951469773530423)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_147 : Polynomial.coeff recurrence2Scalar2Main 147 = -((780658494764747690016024948502562555514 * 10 ^ 70 + 4705516603648887840909095640794803226594653670483289449135095440913868) * 10 ^ 70 + 7106577287613963046912898790509663915390378815683203178771817602063764)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_148 : Polynomial.coeff recurrence2Scalar2Main 148 = (3705006199239753898883764555228773699553 * 10 ^ 70 + 5383313123680731371450007734397092434646756484748037862584329404254954) * 10 ^ 70 + 4629208096938770407116322507446710111130253971794896523251010762255863

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_149 : Polynomial.coeff recurrence2Scalar2Main 149 = -((3804426210447882939389722377704339076802 * 10 ^ 70 + 9987841744811378578931908303967877764563242510117551508689156478220471) * 10 ^ 70 + 9767348835925872997565887806999019076774477618188626667018230939657135)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_150 : Polynomial.coeff recurrence2Scalar2Main 150 = -((36359594917833095547330791554421090653149 * 10 ^ 70 + 135948646196871367641503539129281341297535645592228415771406390427131) * 10 ^ 70 + 5306114728916842743270778324829223191444392845862691456975846151638470)

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_151 : Polynomial.coeff recurrence2Scalar2Main 151 = (193072964510524146736787462491707936393675 * 10 ^ 70 + 4662344836205460422386408764093386339426408855131946017091312275893690) * 10 ^ 70 + 5005352366880257635813860010013269824924818838818699649003159540546045

theorem MazurTorsion.Kubert.OrderSevenBacktrackingCertificate.Internal.ResultantCertificate.recurrence2Scalar2Main_coeff_152 : Polynomial.coeff recurrence2Scalar2Main 152 = -((267384981328010987703676831132499691133977 * 10 ^ 70 + 9302211363535287316829070171709039956522719547159414326601334998664694) * 10 ^ 70 + 1869586802207150520917399614643974583526065845247000523624550591532448)