Quelle  brfac1160   Sprache: Coq

BRENTFACTORS[1160]:=MakeImmutable(
[ ,,,,,,,,,, [ 67153683851 ],, [ 24075709132021 ],,,, [ 15979466282262522097 ]
   ,, [ 1920628637327, 5943086966797 ],, [ 34382149957 ],, 
  [ 39269283037, 64765240783, 876469513819 ],, [ 9719005710501167506301 ], 
  [ 2937066731 ], [ 68715329650237 ],, [ 9984356119 ],,, [ 19963459591553 ], 
  [ 12483990949 ], [ 8162386519127 ], [ 2192150505371 ],, 
  [ 616473180621997, 5034696561987271 ],,, [ 4485587175761 ], 
  [ 891299401467517993981 ],, [ 2055930716469092783 ], 
  [ 15078332112999321596051161 ], [ 2995526251, 7875174080916802696143421 ], 
  [ 1825334712729897143 ], [ 39468434147 ],,,,, [ 47674784872313 ],, 
  [ 13825003267, 49486204423 ], [ 3798925021 ], 
  [ 417476212916008066596335476309074809 ], [ 779774774059 ], 
  [ 2907719674099169, 48045515783444567, 8671810287560536687 ],,,, 
  [ 196098790246921 ],, [ 229498091657805936539842241 ], [ 21888481421 ], 
  [ 881111335567, 274201539496699 ], [ 1025887460113 ], [ 28332304789 ],, 
  [ 6204877771 ], [ 7138159519, 3358496400769 ], 
  [ 563787736562167768938950390611297 ], [ 328465437485993, 626030694910979 ],
  [ 2113898431, 5543899589 ], [ 601669842601 ], 
  [ 2625935129, 31159138237, 11330146666952651009, 97923377866065594739669 ],
  , [ 71861451894396240493 ],, [ 300298951795201 ],, [ 94185990913669957 ],,, 
  [ 2370034749601 ],, [ 533806618041973 ], [ 7525233462209 ], 
  [ 6562138099463 ], [ 7509129931, 16622157980116081, 8491907011997686861 ], 
  [ 2401333785759637 ], [ 22358740589, 2397012980426377 ], [ 304379151487 ],,,
  , [ 2046054757 ], [ 18794396783, 2034907057695166243 ], [ 99444664313083 ],,
  , [ 4259867394606961 ], [ 630840318047 ],, [ 83200011293281 ], 
  [ 14236271171 ],, [ 22212999793 ], [ 358937142100903, 100950520274037389 ], 
  [ 145191892891 ], [ 2784064039 ], [ 6134310449 ], [ 6943509309939496907 ], 
  [ 153027816439 ], [ 356443340881, 10182943062980976971 ],, [ 1328506219 ], 
  [ 410939437432127 ],,, [ 6356009969, 529566666179 ], 
  [ 503035562612147, 10529987849978147 ],,,, [ 2577971528620237 ], 
  [ 64579782975213323 ], [ 124269968513 ],,, 
  [ 291255126719, 420535688968622255213 ], [ 151498863342796201 ], 
  [ 13697950810860317 ],,, [ 1728581892329 ], [ 456249344644686679 ],, 
  [ 2810182183 ],, [ 238008205579, 972177944359, 167725590734701 ], 
  [ 385815838634887 ],, [ 17432225184976993, 5527209712658688433 ], 
  [ 88112169721 ],,,, [ 23574995590446175159 ],,, [ 1381339585361 ],, 
  [ 7635895757029 ],,,,,, [ 9525269571924641 ],, [ 24390668221807051 ],,,, 
  [ 107018905573968287 ],, [ 338735478361800913 ],,,,,, [ 50634602041 ],, 
  [ 1122041009 ],, [ 9304156729117 ],, [ 125041324141, 908124014636765177941 ]
   ,,,,,, [ 1432866067, 273467248184443, 41112054083925478837 ],, 
  [ 2761112573 ],, [ 3693970121, 138795631818401, 655022528190090259781 ],, 
  [ 31174061761 ],, [ 278485857843043, 505257016994202617599591 ],, 
  [ 110312580714169 ],,,,,, [ 78827597059 ],, [ 875013098237815980829 ],, 
  [ 5945268289463, 20938880299742089 ],, 
  [ 30666069117217, 376277930354327992849 ],, [ 1170555121 ],, 
  [ 18239473001, 362122558357530017 ],, [ 2107973647673, 6566752599081061 ],, 
  [ 1780659721, 335656296683741203057 ],,,, [ 2198000641 ],,,,,,,,,,,, 
  [ 1698558769 ],, [ 5830394040901, 50717997983519569 ],, [ 225087076801 ],, 
  [ 8926789818807659 ],,,,,, [ 67897226569 ],,,,,, [ 137333123600251 ],, 
  [ 19962685492501249 ],, [ 7992355873, 25054712147, 26705422333 ],, 
  [ 67922285056715777 ],, [ 1063245110383 ],,,, [ 16150254829 ],,,,,,,,,, 
  [ 6620221045110305921 ],, [ 54016022239379 ],,,, [ 12930769403 ],,,, 
  [ 663383735156948353 ],, [ 1876182768821 ],, [ 70995216929681617 ],, 
  [ 1086344641 ],,,, [ 22383299146981 ],,,, 
  [ 1961529990961, 1096693535416961, 34894520732343957073 ],, 
  [ 3835823616683297 ],,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,
  ,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,
  ,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,
  ,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,, 
  [ 5154677314981 ] ]);