Quelle  brfac639   Sprache: Coq

BRENTFACTORS[639]:=MakeImmutable([ ,,,,,,,,,,,,,,,, [ 8923568690611 ],, 
  [ 3224835953 ],, [ 4928361901 ],,,, [ 2407031651, 1642605136335551 ],, 
  [ 398012903713, 7096527218061847 ],,,,, [ 979239934177 ], [ 184391026051 ], 
  [ 3553650747380291707 ], 
  [ 11945653301, 30392825051, 54274408651, 343813334131 ],, 
  [ 4825785935619664976581249879847, 6471653954645957171528024719960943 ], 
  [ 6725013979003, 34138768392011 ], [ 55755172747, 676013734783366462718899 ]
    , [ 2963433041, 14759265841 ], 
  [ 3395926927, 15401626199614364581, 10222790389176560875903 ],,, 
  [ 26162702149 ], [ 2905901641, 67277495611, 79813828261, 10662108285105631 ]
   ,,,, [ 376942376290745995857787474385341 ], [ 82012474608151 ], 
  [ 262884057627853 ], [ 1022948681, 38427664393 ], 
  [ 92907393771454671091, 2664210732728353974284453214053 ], 
  [ 10085414963149 ], 
  [ 994669396362765795871, 55002402271750365463950764214266921 ],,, 
  [ 333299108753417745756697759259639703401 ], 
  [ 454300493771482904263, 1265346287432865494548954939627, 
      30134066342619056480437875535043034959824240886757937 ], 
  [ 205006279081 ], 
  [ 1249466990011, 587126266077703591, 2186014869682429787, 
      12219470137195101973117811 ],, [ 22388252167 ], 
  [ 2090308795457, 86957887117121 ], 
  [ 1265735761050704711, 666377067398788911278736697621, 
      1701424852215835786058918157221 ], [ 1582649108133914539357 ], 
  [ 211046226610519 ],, [ 1940409307, 13591069381 ], 
  [ 5937736893761, 89323495772081971 ], [ 54134089738153710079237 ],,, 
  [ 650891355094621313, 14571800606727296047740089760189379 ], 
  [ 2802556051 ], [ 44544824307621627040466017746943208401 ], 
  [ 90865728212807124809 ], [ 1547221426366981 ], 
  [ 109853064959615479, 857797065563476383449701 ], 
  [ 15331015178321, 1635715878034241 ], [ 79247783407016211449695381 ], 
  [ 2101603762532041 ], 
  [ 708516363865229, 830720509528271, 1521732580414270093 ],,, 
  [ 2428285939, 27318320827850232251947273 ],, 
  [ 1506721921, 39812666046913, 26913374310654051617, 44114276773135892303993 
     ], [ 2080135373688527 ], [ 90134356097701 ], [ 75221423302553425171 ], 
  [ 56054740537 ], 
  [ 13741031659333518296889199, 274427000481125478652900564537, 
      398065152366915739505598694385058853 ], 
  [ 1153878142097, 555985506256723, 533083776509575129, 
      7729677898017042065807627 ], [ 309801590911 ], 
  [ 88947674770561, 212740744509396731137 ], [ 249086548709 ], 
  [ 340519487603, 7572156933727, 34682552607575280159533237 ], 
  [ 9157276716895354213 ], [ 4101581801, 25656064901 ], [ 1409660916696979 ], 
  [ 454912922333514577 ],, [ 320695529043137, 2199843262410235215593 ], 
  [ 2219658167791, 783523438154521, 190716199253258687692062246421, 
      751491807417559206079436107411 ],, [ 2675792777647577537 ], 
  [ 136299014631433, 2746309242140778781 ], [ 118912827331, 790178272769 ],, 
  [ 8180763355027 ], 
  [ 2033375494456433, 5090620334764277000329200130244737694376968961713 ],, 
  [ 307051825287103559198287, 102371385579002840881639237 ],,, 
  [ 50515570252919324511003575323 ],,, 
  [ 4406129189401, 2233683334684170001, 98370314019229533934441 ], 
  [ 351574569193, 60174004819537093, 1479412578336444801347 ],, 
  [ 46664629537, 3360030561329599 ], [ 6663448604257 ], [ 65216747251 ], 
  [ 289824667241143687593949, 384528412956021507825597509761 ], 
  [ 3809688761874435079 ], [ 42350285569, 2237727082753 ],, 
  [ 47636579854495137841489051, 236232794106556084537888972933207403999161 ],,
  , [ 1243918411 ], [ 234178270076951 ], 
  [ 4973980601753551, 11587105249900441050871 ], 
  [ 61175599153, 159927829121, 1325473039115233, 7500960347365534220089 ], 
  [ 16132799300537, 10232384561669129 ], [ 38812021154077 ],, 
  [ 264723386761, 120999347067832588058354218421088998132503812677321 ], 
  [ 37312488896020159 ], 
  [ 2333505029, 13504667749, 306285984543724979840186458195981331, 
      577866246807127215281186780224032265263894769 ], [ 21282730091741119 ], 
  [ 9783654569235325928077320377986129, 
      21456767574146230345651376919637589404432618801 ],, 
  [ 260463336577, 150100438594240391668421 ],, [ 1435244143543633 ], 
  [ 2175908389, 65686201073148246067, 2964218944327361584709 ], 
  [ 3459042996317305853830876362470869256251 ],, [ 20694334121 ], 
  [ 1088101062146023999258879 ], [ 1434047934551 ],, 
  [ 2401645931783064647617, 538276658589733437759600718375316259037 ],, 
  [ 124154966022149087 ], [ 4557907974200587 ], [ 12573589262009927865352321 ]
   ,, [ 57422507203 ],, [ 13665733093839581, 2389432210574547169 ], 
  [ 8357499151, 1998478581875491, 112178027388886801, 
      94139941899095456916586462891 ], 
  [ 46301459863, 83240284941071, 431495403272963521 ],, 
  [ 2477663161, 691831577821686560161 ],,,,,, 
  [ 60405788678315809, 1750284932813388934672459 ],,,, 
  [ 2237111299, 14937506669867 ],,,, [ 728741328994667641693850993 ], 
  [ 349738130293, 127004219065964893 ], [ 3369489881, 5696740649 ],, 
  [ 189088027962216572790709 ],,,,,, [ 5723171521 ],,, 
  [ 126560525911, 5261025457651483651 ], [ 13255489489733 ],, 
  [ 547988019397235803 ],, [ 1833468734343554384801 ],, 
  [ 1274750089, 1213141910243 ],,,,,,,, 
  [ 746172670576099816800732915516167302504336038180902523557071381 ],,,,,,,, 
  [ 2337591329 ],,,, [ 2376089311, 4027821037, 1183346300847943103644972879 ],
  ,,, [ 17330720279, 1607795602298681, 1125222725920946207 ],, 
  [ 73270970383777, 127938231626964470329 ],, 
  [ 46102920401, 41425970878031, 799464555952411 ], [ 268181702251 ], 
  [ 5989545857, 383770848188809 ],, [ 3274086583, 7008546403 ],, 
  [ 79603218618200464665869 ],,,, [ 1145403912653215369378801 ],, 
  [ 2168843447, 30107697709 ],, 
  [ 71804736035861, 468349393438753, 76930225904517473 ],, [ 3452339263717 ],
  , [ 151711375391201 ],, [ 1146961675205543240501 ],, [ 31341200346412741 ],,
  ,,,,,,,,,, [ 8691976814401 ],, [ 578894009429513 ],, 
  [ 23119201169, 31510882561, 33566808685789 ],, 
  [ 5434427701, 61192763891011 ],,,, [ 4027075271 ],,,, [ 12462345619393829 ],
  , [ 479791886285472333161, 93963148175918117851441 ],, [ 10667268427 ],,,, 
  [ 32598984724028227649 ],, [ 149215555202977 ],, [ 32697222203534951 ],,,, 
  [ 127104288823 ],,,,,, [ 185848170063901, 46422391799818037493358201 ],,,,,
  , [ 2404333801, 5793505651, 14699998567, 136283598523, 559262938879, 
      1409052194911, 112476716735864077, 17458275976377427567 ],, 
  [ 11079741417053 ],,,, 
  [ 20601559681, 922053099641924641, 265487702796475330147393 ],,,,,, 
  [ 6150315889 ],,,,,, [ 2656926361 ],,,,,, [ 31840697099311 ],,,,,, 
  [ 2580622681393 ],,,,,, [ 1359170406716663557, 30711414178663744213 ],,,,,, 
  [ 732167032741, 806667425536261 ],, [ 1321203368801 ],, [ 23175348302657 ],
  , [ 8238805903 ],,,,,,,,,,,,,,,,,,,,,,,, [ 7462822249 ],,,,,, 
  [ 9139846657, 236436686209 ],,,,,, [ 3676716811 ],,,,,,,,,,,,,,,,,,,,,,,,,,,
  ,,, [ 1340517361, 5720374748860801, 614970255201101941 ],,,,,, 
  [ 36496920799 ],,,,,,,,,,,,,,,,,,,,,,,, [ 2559298051 ],,,,,,,,,,,,,,,,,,,,,,
  ,,,,,,,, [ 106641896758202881 ] ]);