Factor utility lemmas from x86 out of asm files

Also add some lemmas for compat of x86 branch with 8.11

<details><summary>Timing Diff</summary>
<p>

```
    After |   Peak Mem | File Name                                                       |    Before |   Peak Mem ||    Change || Change (mem) | % Change | % Change (mem)
--------------------------------------------------------------------------------------------------------------------------------------------------------------------------
61m30.85s | 1990484 ko | Total Time / Peak Mem                                           | 61m25.90s | 1991316 ko || +0m04.94s ||      -832 ko |   +0.13% |         -0.04%
--------------------------------------------------------------------------------------------------------------------------------------------------------------------------
 1m28.11s | 1516788 ko | SlowPrimeSynthesisExamples.vo                                   |  1m25.30s | 1516872 ko || +0m02.81s ||       -84 ko |   +3.29% |         -0.00%
 3m18.24s | 1702064 ko | Curves/Montgomery/XZProofs.vo                                   |  3m16.75s | 1640968 ko || +0m01.49s ||     61096 ko |   +0.75% |         +3.72%
 4m21.92s | 1350984 ko | PushButtonSynthesis/WordByWordMontgomeryReificationCache.vo     |  4m21.95s | 1370208 ko || -0m00.02s ||    -19224 ko |   -0.01% |         -1.40%
 3m49.43s | 1990484 ko | Rewriter/Passes/ArithWithCasts.vo                               |  3m49.56s | 1991316 ko || -0m00.12s ||      -832 ko |   -0.05% |         -0.04%
 3m04.56s | 1609256 ko | Rewriter/Passes/NBE.vo                                          |  3m04.56s | 1609184 ko || +0m00.00s ||        72 ko |   +0.00% |         +0.00%
 2m51.21s | 1176040 ko | Fancy/Compiler.vo                                               |  2m51.21s | 1176784 ko || +0m00.00s ||      -744 ko |   +0.00% |         -0.06%
 2m27.09s | 1765524 ko | Rewriter/Passes/ToFancyWithCasts.vo                             |  2m27.13s | 1621832 ko || -0m00.03s ||    143692 ko |   -0.02% |         +8.85%
 2m18.79s |  933052 ko | AbstractInterpretation/Wf.vo                                    |  2m18.92s |  934624 ko || -0m00.13s ||     -1572 ko |   -0.09% |         -0.16%
 2m00.23s | 1042084 ko | Bedrock/Field/Synthesis/Examples/X25519_64.vo                   |  1m59.90s | 1042060 ko || +0m00.32s ||        24 ko |   +0.27% |         +0.00%
 1m49.43s | 1213588 ko | Bedrock/Group/ScalarMult/LadderStep.vo                          |  1m49.31s | 1285028 ko || +0m00.12s ||    -71440 ko |   +0.10% |         -5.55%
 1m38.44s |  434576 ko | Spec/Test/X25519.vo                                             |  1m38.41s |  434468 ko || +0m00.03s ||       108 ko |   +0.03% |         +0.02%
 1m37.11s | 1434840 ko | Fancy/Barrett256.vo                                             |  1m37.05s | 1397932 ko || +0m00.06s ||     36908 ko |   +0.06% |         +2.64%
 1m15.51s | 1130132 ko | UnsaturatedSolinasHeuristics/Tests.vo                           |  1m15.22s | 1130096 ko || +0m00.29s ||        36 ko |   +0.38% |         +0.00%
 1m14.09s | 1317332 ko | Bedrock/Field/Synthesis/Generic/UnsaturatedSolinas.vo           |  1m14.29s | 1317232 ko || -0m00.19s ||       100 ko |   -0.26% |         +0.00%
 1m12.98s |  791080 ko | AbstractInterpretation/Proofs.vo                                |  1m12.87s |  797516 ko || +0m00.10s ||     -6436 ko |   +0.15% |         -0.80%
 1m11.33s | 1285096 ko | Bedrock/Field/Synthesis/Generic/WordByWordMontgomery.vo         |  1m11.37s | 1288764 ko || -0m00.04s ||     -3668 ko |   -0.05% |         -0.28%
 1m08.57s |  856328 ko | AbstractInterpretation/ZRangeProofs.vo                          |  1m08.90s |  855948 ko || -0m00.33s ||       380 ko |   -0.47% |         +0.04%
 1m04.54s | 1436764 ko | Bedrock/Field/Synthesis/Examples/p224_64.vo                     |  1m04.53s | 1436720 ko || +0m00.01s ||        44 ko |   +0.01% |         +0.00%
 1m02.97s | 1406988 ko | Bedrock/Field/Synthesis/Examples/p256_64.vo                     |  1m03.14s | 1406892 ko || -0m00.17s ||        96 ko |   -0.26% |         +0.00%
 1m01.76s | 1327100 ko | Fancy/Montgomery256.vo                                          |  1m01.74s | 1345380 ko || +0m00.01s ||    -18280 ko |   +0.03% |         -1.35%
 1m00.99s |  928944 ko | PushButtonSynthesis/UnsaturatedSolinasReificationCache.vo       |  1m00.86s |  928892 ko || +0m00.13s ||        52 ko |   +0.21% |         +0.00%
 1m00.84s | 1120888 ko | Bedrock/Field/Translation/Proofs/ValidComputable/Expr.vo        |  1m00.54s | 1120708 ko || +0m00.30s ||       180 ko |   +0.49% |         +0.01%
 1m00.79s | 1038612 ko | Rewriter/Passes/MultiRetSplit.vo                                |  1m00.69s | 1036692 ko || +0m00.10s ||      1920 ko |   +0.16% |         +0.18%
 0m54.44s |  776008 ko | Rewriter/RulesProofs.vo                                         |  0m54.41s |  771220 ko || +0m00.03s ||      4788 ko |   +0.05% |         +0.62%
 0m53.67s | 1123148 ko | Rewriter/Passes/Arith.vo                                        |  0m53.57s | 1123208 ko || +0m00.10s ||       -60 ko |   +0.18% |         -0.00%
 0m46.61s |  622308 ko | Demo.vo                                                         |  0m47.43s |  624428 ko || -0m00.82s ||     -2120 ko |   -1.72% |         -0.33%
 0m42.36s |  854840 ko | Bedrock/Field/Synthesis/Examples/LadderStep.vo                  |  0m42.49s |  855052 ko || -0m00.13s ||      -212 ko |   -0.30% |         -0.02%
 0m36.57s |  891372 ko | Rewriter/Passes/MulSplit.vo                                     |  0m36.54s |  890896 ko || +0m00.03s ||       476 ko |   +0.08% |         +0.05%
 0m31.19s |  880480 ko | Bedrock/Field/Synthesis/New/UnsaturatedSolinas.vo               |  0m31.04s |  880640 ko || +0m00.15s ||      -160 ko |   +0.48% |         -0.01%
 0m31.08s |  523240 ko | Arithmetic/Saturated.vo                                         |  0m31.15s |  523384 ko || -0m00.07s ||      -144 ko |   -0.22% |         -0.02%
 0m30.39s |  934236 ko | PushButtonSynthesis/BYInversionReificationCache.vo              |  0m30.38s |  934176 ko || +0m00.01s ||        60 ko |   +0.03% |         +0.00%
 0m28.85s |  852056 ko | PushButtonSynthesis/UnsaturatedSolinas.vo                       |  0m28.82s |  851796 ko || +0m00.03s ||       260 ko |   +0.10% |         +0.03%
 0m28.16s |  891892 ko | PushButtonSynthesis/BarrettReductionReificationCache.vo         |  0m28.11s |  891756 ko || +0m00.05s ||       136 ko |   +0.17% |         +0.01%
 0m26.24s | 1071932 ko | Assembly/Parse/TestAsm.vo                                       |  0m26.14s | 1071820 ko || +0m00.09s ||       112 ko |   +0.38% |         +0.01%
 0m23.15s |  872612 ko | PushButtonSynthesis/WordByWordMontgomery.vo                     |  0m23.21s |  871584 ko || -0m00.06s ||      1028 ko |   -0.25% |         +0.11%
 0m21.01s |  794684 ko | Bedrock/Field/Translation/Proofs/Expr.vo                        |  0m20.89s |  788616 ko || +0m00.12s ||      6068 ko |   +0.57% |         +0.76%
 0m20.13s |  831868 ko | Bedrock/Field/Synthesis/Examples/X1305_32.vo                    |  0m19.99s |  831944 ko || +0m00.14s ||       -76 ko |   +0.70% |         -0.00%
 0m17.61s |  544676 ko | Arithmetic/BarrettReduction.vo                                  |  0m17.43s |  543440 ko || +0m00.17s ||      1236 ko |   +1.03% |         +0.22%
 0m17.31s |  576056 ko | Arithmetic/WordByWordMontgomery.vo                              |  0m17.25s |  570092 ko || +0m00.05s ||      5964 ko |   +0.34% |         +1.04%
 0m17.14s |  853912 ko | Curves/Edwards/XYZT/Basic.vo                                    |  0m16.96s |  853168 ko || +0m00.17s ||       744 ko |   +1.06% |         +0.08%
 0m17.04s |  709932 ko | Bedrock/Field/Translation/Proofs/LoadStoreList.vo               |  0m17.15s |  709848 ko || -0m00.10s ||        84 ko |   -0.64% |         +0.01%
 0m16.87s |  648496 ko | Util/ZUtil/ArithmeticShiftr.vo                                  |  0m16.81s |  648796 ko || +0m00.06s ||      -300 ko |   +0.35% |         -0.04%
 0m16.70s |  515116 ko | Arithmetic/Core.vo                                              |  0m16.56s |  515192 ko || +0m00.14s ||       -76 ko |   +0.84% |         -0.01%
 0m16.69s |  795996 ko | PushButtonSynthesis/FancyMontgomeryReductionReificationCache.vo |  0m16.43s |  802952 ko || +0m00.26s ||     -6956 ko |   +1.58% |         -0.86%
 0m16.58s |  772104 ko | Language/IdentifiersGENERATED.vo                                |  0m16.52s |  772196 ko || +0m00.05s ||       -92 ko |   +0.36% |         -0.01%
 0m16.05s |  631640 ko | Bedrock/Field/Common/Util.vo                                    |  0m15.91s |  631508 ko || +0m00.14s ||       132 ko |   +0.87% |         +0.02%
 0m15.91s |  717092 ko | Curves/Edwards/AffineProofs.vo                                  |  0m15.86s |  717008 ko || +0m00.05s ||        84 ko |   +0.31% |         +0.01%
 0m15.21s |  584124 ko | Stringification/IR.vo                                           |  0m15.17s |  583972 ko || +0m00.04s ||       152 ko |   +0.26% |         +0.02%
 0m14.51s |  871992 ko | StandaloneDebuggingExamples.vo                                  |  0m14.60s |  871788 ko || -0m00.08s ||       204 ko |   -0.61% |         +0.02%
 0m13.44s |  597140 ko | Language/IdentifiersGENERATEDProofs.vo                          |  0m13.91s |  596824 ko || -0m00.47s ||       316 ko |   -3.37% |         +0.05%
 0m13.38s |  774580 ko | Bedrock/Field/Translation/Proofs/Cmd.vo                         |  0m13.46s |  774652 ko || -0m00.08s ||       -72 ko |   -0.59% |         -0.00%
 0m12.85s |  753740 ko | Bedrock/Field/Synthesis/New/Signature.vo                        |  0m12.86s |  753808 ko || -0m00.00s ||       -68 ko |   -0.07% |         -0.00%
 0m12.14s |  684432 ko | Bedrock/Field/Translation/Proofs/ValidComputable/Cmd.vo         |  0m12.09s |  684092 ko || +0m00.05s ||       340 ko |   +0.41% |         +0.04%
 0m12.13s |  610120 ko | Util/ZRange/LandLorBounds.vo                                    |  0m12.04s |  609660 ko || +0m00.09s ||       460 ko |   +0.74% |         +0.07%
 0m11.66s |  862584 ko | PushButtonSynthesis/SmallExamples.vo                            |  0m11.25s |  862320 ko || +0m00.41s ||       264 ko |   +3.64% |         +0.03%
 0m11.13s |  478384 ko | Primitives/MxDHRepChange.vo                                     |  0m11.18s |  478448 ko || -0m00.04s ||       -64 ko |   -0.44% |         -0.01%
 0m09.27s |  496716 ko | Arithmetic/FancyMontgomeryReduction.vo                          |  0m09.29s |  495060 ko || -0m00.01s ||      1656 ko |   -0.21% |         +0.33%
 0m09.11s |  748216 ko | Bedrock/Field/Translation/Proofs/Func.vo                        |  0m08.97s |  746784 ko || +0m00.13s ||      1432 ko |   +1.56% |         +0.19%
 0m08.94s |  599776 ko | Language/IdentifiersBasicGENERATED.vo                           |  0m09.01s |  599956 ko || -0m00.07s ||      -180 ko |   -0.77% |         -0.03%
 0m08.91s |  598964 ko | Rewriter/Passes/RelaxBitwidthAdcSbb.vo                          |  0m08.92s |  598940 ko || -0m00.00s ||        24 ko |   -0.11% |         +0.00%
 0m08.01s |  919520 ko | Bedrock/Field/Translation/Proofs/EquivalenceProperties.vo       |  0m07.99s |  919420 ko || +0m00.01s ||       100 ko |   +0.25% |         +0.01%
 0m07.96s |  486892 ko | Util/ZRange/CornersMonotoneBounds.vo                            |  0m07.99s |  486792 ko || -0m00.03s ||       100 ko |   -0.37% |         +0.02%
 0m07.90s |  620364 ko | Bedrock/Field/Translation/Proofs/Flatten.vo                     |  0m07.97s |  620296 ko || -0m00.06s ||        68 ko |   -0.87% |         +0.01%
 0m07.85s |  694052 ko | PushButtonSynthesis/BaseConversion.vo                           |  0m07.97s |  693928 ko || -0m00.12s ||       124 ko |   -1.50% |         +0.01%
 0m07.64s |  614616 ko | Bedrock/Group/ScalarMult/ScalarMult.vo                          |  0m07.70s |  614484 ko || -0m00.06s ||       132 ko |   -0.77% |         +0.02%
 0m07.01s |  569692 ko | Rewriter/Passes/NoSelect.vo                                     |  0m06.93s |  569096 ko || +0m00.08s ||       596 ko |   +1.15% |         +0.10%
 0m06.66s |  706040 ko | PushButtonSynthesis/Primitives.vo                               |  0m06.64s |  706056 ko || +0m00.02s ||       -16 ko |   +0.30% |         -0.00%
 0m06.50s |  600068 ko | PushButtonSynthesis/SaturatedSolinasReificationCache.vo         |  0m06.41s |  599968 ko || +0m00.08s ||       100 ko |   +1.40% |         +0.01%
 0m06.38s |  939028 ko | Bedrock/Field/Translation/Proofs/UsedVarnames.vo                |  0m06.44s |  939032 ko || -0m00.06s ||        -4 ko |   -0.93% |         -0.00%
 0m05.83s |  499848 ko | Util/ZUtil/Modulo.vo                                            |  0m05.73s |  499632 ko || +0m00.09s ||       216 ko |   +1.74% |         +0.04%
 0m05.81s |  541936 ko | Arithmetic/BYInv.vo                                             |  0m05.84s |  541648 ko || -0m00.03s ||       288 ko |   -0.51% |         +0.05%
 0m05.61s |  738192 ko | Bedrock/Field/Synthesis/Examples/EncodeDecode.vo                |  0m05.59s |  738220 ko || +0m00.02s ||       -28 ko |   +0.35% |         -0.00%
 0m05.52s |  548784 ko | Language/InversionExtra.vo                                      |  0m05.34s |  545900 ko || +0m00.17s ||      2884 ko |   +3.37% |         +0.52%
 0m05.49s |  624900 ko | BoundsPipeline.vo                                               |  0m05.46s |  624776 ko || +0m00.03s ||       124 ko |   +0.54% |         +0.01%
 0m05.40s |  520816 ko | COperationSpecifications.vo                                     |  0m05.42s |  520772 ko || -0m00.01s ||        44 ko |   -0.36% |         +0.00%
 0m05.17s |  558312 ko | Fancy/Prod.vo                                                   |  0m05.24s |  558392 ko || -0m00.07s ||       -80 ko |   -1.33% |         -0.01%
 0m04.98s |  631904 ko | Assembly/Syntax.vo                                              |  0m04.98s |  631380 ko || +0m00.00s ||       524 ko |   +0.00% |         +0.08%
 0m04.74s |  462548 ko | Arithmetic/MontgomeryReduction/Proofs.vo                        |  0m04.79s |  462520 ko || -0m00.04s ||        28 ko |   -1.04% |         +0.00%
 0m04.73s |  688060 ko | PushButtonSynthesis/BarrettReduction.vo                         |  0m04.78s |  687720 ko || -0m00.04s ||       340 ko |   -1.04% |         +0.04%
 0m04.57s |  490360 ko | UnsaturatedSolinasHeuristics.vo                                 |  0m04.58s |  489520 ko || -0m00.00s ||       840 ko |   -0.21% |         +0.17%
 0m04.34s |  491352 ko | Util/ZRange/BasicLemmas.vo                                      |  0m04.42s |  491136 ko || -0m00.08s ||       216 ko |   -1.80% |         +0.04%
 0m03.80s |  479516 ko | Arithmetic/UniformWeight.vo                                     |  0m03.82s |  478644 ko || -0m00.02s ||       872 ko |   -0.52% |         +0.18%
 0m03.74s |  478744 ko | Arithmetic/BarrettReduction/Generalized.vo                      |  0m03.78s |  478724 ko || -0m00.03s ||        20 ko |   -1.05% |         +0.00%
 0m03.70s |  702764 ko | Bedrock/Field/Synthesis/Examples/MulTwice.vo                    |  0m03.77s |  702796 ko || -0m00.06s ||       -32 ko |   -1.85% |         -0.00%
 0m03.67s |  476992 ko | CastLemmas.vo                                                   |  0m03.58s |  476964 ko || +0m00.08s ||        28 ko |   +2.51% |         +0.00%
 0m03.46s |  558456 ko | PushButtonSynthesis/BaseConversionReificationCache.vo           |  0m03.43s |  558280 ko || +0m00.02s ||       176 ko |   +0.87% |         +0.03%
 0m03.37s |  701092 ko | PushButtonSynthesis/FancyMontgomeryReduction.vo                 |  0m03.48s |  701000 ko || -0m00.10s ||        92 ko |   -3.16% |         +0.01%
 0m03.31s |  508260 ko | Assembly/Semantics.vo                                           |  0m03.21s |  508316 ko || +0m00.10s ||       -56 ko |   +3.11% |         -0.01%
 0m03.31s |  522400 ko | Rewriter/Passes/Test.vo                                         |  0m03.31s |  522408 ko || +0m00.00s ||        -8 ko |   +0.00% |         -0.00%
 0m03.31s |  481420 ko | Util/ZUtil/LandLorBounds.vo                                     |  0m03.32s |  481828 ko || -0m00.00s ||      -408 ko |   -0.30% |         -0.08%
 0m03.27s |  685920 ko | PushButtonSynthesis/SaturatedSolinas.vo                         |  0m03.29s |  685724 ko || -0m00.02s ||       196 ko |   -0.60% |         +0.02%
 0m03.21s |  533872 ko | Rewriter/Passes/AddAssocLeft.vo                                 |  0m03.18s |  533704 ko || +0m00.02s ||       168 ko |   +0.94% |         +0.03%
 0m03.13s |  471776 ko | Util/ZUtil/LandLorShiftBounds.vo                                |  0m03.17s |  472456 ko || -0m00.04s ||      -680 ko |   -1.26% |         -0.14%
 0m03.11s |  471740 ko | Arithmetic/BarrettReduction/HAC.vo                              |  0m03.09s |  471264 ko || +0m00.02s ||       476 ko |   +0.64% |         +0.10%
 0m02.89s |  696520 ko | CLI.vo                                                          |  0m02.92s |  696384 ko || -0m00.02s ||       136 ko |   -1.02% |         +0.01%
 0m02.81s |  533152 ko | Rewriter/Passes/FlattenThunkedRects.vo                          |  0m02.92s |  533304 ko || -0m00.10s ||      -152 ko |   -3.76% |         -0.02%
 0m02.63s |  503896 ko | Util/ZUtil/Morphisms.vo                                         |  0m02.63s |  503864 ko || +0m00.00s ||        32 ko |   +0.00% |         +0.00%
 0m02.57s |  464304 ko | Arithmetic/Primitives.vo                                        |  0m02.59s |  464028 ko || -0m00.02s ||       276 ko |   -0.77% |         +0.05%
 0m02.37s |  480652 ko | Arithmetic/Freeze.vo                                            |  0m02.33s |  479460 ko || +0m00.04s ||      1192 ko |   +1.71% |         +0.24%
 0m02.31s |  465796 ko | Util/ZUtil/TwosComplement.vo                                    |  0m02.31s |  465692 ko || +0m00.00s ||       104 ko |   +0.00% |         +0.02%
 0m02.28s |  468932 ko | Util/ZUtil/Shift.vo                                             |  0m02.26s |  468988 ko || +0m00.02s ||       -56 ko |   +0.88% |         -0.01%
 0m02.27s |  620024 ko | Bedrock/Field/Common/Arrays/MakeAccessSizes.vo                  |  0m02.30s |  620032 ko || -0m00.02s ||        -8 ko |   -1.30% |         -0.00%
 0m02.17s |  472028 ko | Arithmetic/BaseConversion.vo                                    |  0m02.12s |  471888 ko || +0m00.04s ||       140 ko |   +2.35% |         +0.02%
 0m02.17s |  530996 ko | Rewriter/Passes/UnfoldValueBarrier.vo                           |  0m02.25s |  530896 ko || -0m00.08s ||       100 ko |   -3.55% |         +0.01%
 0m02.12s |  535208 ko | Bedrock/Field/Translation/Expr.vo                               |  0m02.15s |  535144 ko || -0m00.02s ||        64 ko |   -1.39% |         +0.01%
 0m02.07s |  530948 ko | Rewriter/Passes/StripLiteralCasts.vo                            |  0m02.02s |  530792 ko || +0m00.04s ||       156 ko |   +2.47% |         +0.02%
 0m02.04s |  458040 ko | Util/ZUtil/Testbit.vo                                           |  0m02.07s |  458036 ko || -0m00.02s ||         4 ko |   -1.44% |         +0.00%
 0m02.00s |  454608 ko | Util/ZUtil/ModInv.vo                                            |  0m02.11s |  457112 ko || -0m00.10s ||     -2504 ko |   -5.21% |         -0.54%
 0m01.96s |  457568 ko | Util/ZUtil/Div.vo                                               |  0m01.96s |  457820 ko || +0m00.00s ||      -252 ko |   +0.00% |         -0.05%
 0m01.94s |  554116 ko | Stringification/Language.vo                                     |  0m02.00s |  554072 ko || -0m00.06s ||        44 ko |   -3.00% |         +0.00%
 0m01.92s |  456528 ko | Arithmetic/BarrettReduction/RidiculousFish.vo                   |  0m01.93s |  456388 ko || -0m00.01s ||       140 ko |   -0.51% |         +0.03%
 0m01.89s |  476704 ko | Arithmetic/ModOps.vo                                            |  0m01.92s |  476780 ko || -0m00.03s ||       -76 ko |   -1.56% |         -0.01%
 0m01.83s |  581544 ko | CompilersTestCases.vo                                           |  0m01.85s |  584836 ko || -0m00.02s ||     -3292 ko |   -1.08% |         -0.56%
 0m01.80s |  466128 ko | Arithmetic/ModularArithmeticTheorems.vo                         |  0m01.94s |  466236 ko || -0m00.13s ||      -108 ko |   -7.21% |         -0.02%
 0m01.76s |  454524 ko | Util/Tuple.vo                                                   |  0m01.76s |  455292 ko || +0m00.00s ||      -768 ko |   +0.00% |         -0.16%
 0m01.74s |  506628 ko | AbstractInterpretation/AbstractInterpretation.vo                |  0m01.76s |  506536 ko || -0m00.02s ||        92 ko |   -1.13% |         +0.01%
 0m01.73s |  529296 ko | Rewriter/Passes/ToFancy.vo                                      |  0m01.83s |  529176 ko || -0m00.10s ||       120 ko |   -5.46% |         +0.02%
 0m01.71s |  536504 ko | AbstractInterpretation/ZRange.vo                                |  0m01.75s |  536588 ko || -0m00.04s ||       -84 ko |   -2.28% |         -0.01%
 0m01.62s |  619728 ko | Bedrock/Field/Common/Names/MakeNames.vo                         |  0m01.67s |  619760 ko || -0m00.04s ||       -32 ko |   -2.99% |         -0.00%
 0m01.61s |  494640 ko | Bedrock/Field/Interface/Compilation.vo                          |  0m01.60s |  494616 ko || +0m00.01s ||        24 ko |   +0.62% |         +0.00%
 0m01.61s |  697828 ko | Rewriter/PerfTesting/Core.vo                                    |  0m01.62s |  697864 ko || -0m00.01s ||       -36 ko |   -0.61% |         -0.00%
 0m01.54s |  521944 ko | Stringification/Go.vo                                           |  0m01.49s |  522556 ko || +0m00.05s ||      -612 ko |   +3.35% |         -0.11%
 0m01.53s |  457796 ko | Util/ZUtil/Pow2Mod.vo                                           |  0m01.51s |  457856 ko || +0m00.02s ||       -60 ko |   +1.32% |         -0.01%
 0m01.52s |  630524 ko | Bedrock/Field/Synthesis/Generic/Bignum.vo                       |  0m01.44s |  629852 ko || +0m00.08s ||       672 ko |   +5.55% |         +0.10%
 0m01.52s |  537472 ko | Bedrock/Group/ScalarMult/MontgomeryEquivalence.vo               |  0m01.48s |  537464 ko || +0m00.04s ||         8 ko |   +2.70% |         +0.00%
 0m01.51s |  465372 ko | Assembly/Parse.vo                                               |  0m01.59s |  465668 ko || -0m00.08s ||      -296 ko |   -5.03% |         -0.06%
 0m01.45s |  471620 ko | Util/ZRange/SplitRangeBounds.vo                                 |  0m01.46s |  471604 ko || -0m00.01s ||        16 ko |   -0.68% |         +0.00%
 0m01.42s |  704852 ko | Rewriter/PerfTesting/StandaloneOCamlMain.vo                     |  0m01.39s |  704764 ko || +0m00.03s ||        88 ko |   +2.15% |         +0.01%
 0m01.41s |  502200 ko | Bedrock/Group/ScalarMult/MontgomeryLadder.vo                    |  0m01.51s |  502060 ko || -0m00.10s ||       140 ko |   -6.62% |         +0.02%
 0m01.41s |  464600 ko | Util/ZUtil/Bitwise.vo                                           |  0m01.45s |  464460 ko || -0m00.04s ||       140 ko |   -2.75% |         +0.03%
 0m01.35s |  503408 ko | Arithmetic/PrimeFieldTheorems.vo                                |  0m01.25s |  503744 ko || +0m00.10s ||      -336 ko |   +8.00% |         -0.06%
 0m01.29s |  617364 ko | Bedrock/Field/Common/Arrays/MaxBounds.vo                        |  0m01.37s |  617436 ko || -0m00.08s ||       -72 ko |   -5.83% |         -0.01%
 0m01.28s |  468428 ko | Util/ZUtil/Quot.vo                                              |  0m01.28s |  468296 ko || +0m00.00s ||       132 ko |   +0.00% |         +0.02%
 0m01.23s |  461340 ko | Arithmetic/Partition.vo                                         |  0m01.23s |  461124 ko || +0m00.00s ||       216 ko |   +0.00% |         +0.04%
 0m01.18s |  455968 ko | Util/ZUtil/Ones.vo                                              |  0m01.09s |  455832 ko || +0m00.08s ||       136 ko |   +8.25% |         +0.02%
 0m01.17s |  444308 ko | Fancy/Spec.vo                                                   |  0m01.15s |  444352 ko || +0m00.02s ||       -44 ko |   +1.73% |         -0.00%
 0m01.14s |  635044 ko | Bedrock/Field/Interface/Representation.vo                       |  0m01.06s |  634616 ko || +0m00.07s ||       428 ko |   +7.54% |         +0.06%
 0m01.14s |  680088 ko | Bedrock/Field/Stringification/Stringification.vo                |  0m01.15s |  680040 ko || -0m00.01s ||        48 ko |   -0.86% |         +0.00%
 0m01.13s |  671752 ko | Bedrock/Field/Synthesis/Generic/Tactics.vo                      |  0m01.06s |  671640 ko || +0m00.06s ||       112 ko |   +6.60% |         +0.01%
 0m01.13s |  703676 ko | Bedrock/Field/Synthesis/Specialized/WordByWordMontgomery.vo     |  0m01.14s |  703560 ko || -0m00.01s ||       116 ko |   -0.87% |         +0.01%
 0m01.12s |  692472 ko | Bedrock/Field/Synthesis/Specialized/UnsaturatedSolinas.vo       |  0m01.12s |  692268 ko || +0m00.00s ||       204 ko |   +0.00% |         +0.02%
 0m01.12s |  473096 ko | Util/ZRange/SplitBounds.vo                                      |  0m01.14s |  473104 ko || -0m00.01s ||        -8 ko |   -1.75% |         -0.00%
 0m01.12s |  449856 ko | Util/ZUtil/AddGetCarry.vo                                       |  0m01.15s |  450052 ko || -0m00.02s ||      -196 ko |   -2.60% |         -0.04%
 0m01.11s |  611772 ko | Bedrock/Field/Common/Arrays/ByteBounds.vo                       |  0m01.05s |  611932 ko || +0m00.06s ||      -160 ko |   +5.71% |         -0.02%
 0m01.10s |  676524 ko | Bedrock/Field/Translation/Proofs/ValidComputable/Func.vo        |  0m01.12s |  676356 ko || -0m00.02s ||       168 ko |   -1.78% |         +0.02%
 0m01.10s |  712464 ko | Bedrock/Standalone/StandaloneOCamlMain.vo                       |  0m01.09s |  712620 ko || +0m00.01s ||      -156 ko |   +0.91% |         -0.02%
 0m01.09s |  672372 ko | Bedrock/Field/Synthesis/Specialized/Tactics.vo                  |  0m00.91s |  672380 ko || +0m00.18s ||        -8 ko |  +19.78% |         -0.00%
 0m01.08s |  675140 ko | Bedrock/Field/Synthesis/Generic/Operation.vo                    |  0m01.07s |  675244 ko || +0m00.01s ||      -104 ko |   +0.93% |         -0.01%
 0m01.08s |  618104 ko | Bedrock/Field/Translation/Cmd.vo                                |  0m01.20s |  618396 ko || -0m00.11s ||      -292 ko |   -9.99% |         -0.04%
 0m01.05s |  424760 ko | Util/ZUtil/OnesFrom.vo                                          |  0m01.07s |  424684 ko || -0m00.02s ||        76 ko |   -1.86% |         +0.01%
 0m01.04s |  712232 ko | Bedrock/Standalone/StandaloneHaskellMain.vo                     |  0m01.04s |  712140 ko || +0m00.00s ||        92 ko |   +0.00% |         +0.01%
 0m01.04s |  437920 ko | Curves/Edwards/XYZT/Precomputed.vo                              |  0m01.21s |  438028 ko || -0m00.16s ||      -108 ko |  -14.04% |         -0.02%
 0m01.04s |  689692 ko | StandaloneOCamlMain.vo                                          |  0m01.05s |  689504 ko || -0m00.01s ||       188 ko |   -0.95% |         +0.02%
 0m01.03s |  520256 ko | Stringification/JSON.vo                                         |  0m01.19s |  519884 ko || -0m00.15s ||       372 ko |  -13.44% |         +0.07%
 0m01.02s |  632612 ko | Bedrock/Field/Translation/Parameters/SelectParameters.vo        |  0m00.96s |  632620 ko || +0m00.06s ||        -8 ko |   +6.25% |         -0.00%
 0m01.01s |  688788 ko | StandaloneHaskellMain.vo                                        |  0m01.05s |  688876 ko || -0m00.04s ||       -88 ko |   -3.80% |         -0.01%
 0m01.00s |  681844 ko | Bedrock/Field/Synthesis/New/ComputedOp.vo                       |  0m01.09s |  681808 ko || -0m00.09s ||        36 ko |   -8.25% |         +0.00%
 0m00.97s |  682240 ko | Bedrock/Field/Synthesis/Specialized/ReifiedOperation.vo         |  0m01.01s |  682068 ko || -0m00.04s ||       172 ko |   -3.96% |         +0.02%
 0m00.97s |  631772 ko | Bedrock/Field/Translation/Parameters/Defaults32.vo              |  0m00.99s |  631568 ko || -0m00.02s ||       204 ko |   -2.02% |         +0.03%
 0m00.96s |  617480 ko | Bedrock/Field/Translation/Func.vo                               |  0m00.92s |  617356 ko || +0m00.03s ||       124 ko |   +4.34% |         +0.02%
 0m00.96s |  631492 ko | Bedrock/Field/Translation/Parameters/Defaults64.vo              |  0m00.96s |  631584 ko || +0m00.00s ||       -92 ko |   +0.00% |         -0.01%
 0m00.95s |  519120 ko | Stringification/C.vo                                            |  0m00.99s |  519080 ko || -0m00.04s ||        40 ko |   -4.04% |         +0.00%
 0m00.94s |  550372 ko | Assembly/Equivalence.vo                                         |  0m01.02s |  550652 ko || -0m00.08s ||      -280 ko |   -7.84% |         -0.05%
 0m00.92s |  520072 ko | Stringification/Zig.vo                                          |  0m00.93s |  520032 ko || -0m00.01s ||        40 ko |   -1.07% |         +0.00%
 0m00.89s |  629652 ko | Bedrock/Field/Translation/Parameters/Defaults.vo                |  0m00.95s |  629328 ko || -0m00.05s ||       324 ko |   -6.31% |         +0.05%
 0m00.86s |  519424 ko | Stringification/Rust.vo                                         |  0m00.91s |  519212 ko || -0m00.05s ||       212 ko |   -5.49% |         +0.04%
 0m00.86s |  456284 ko | Util/ZUtil/TruncatingShiftl.vo                                  |  0m00.81s |  456092 ko || +0m00.04s ||       192 ko |   +6.17% |         +0.04%
 0m00.85s |  519164 ko | Stringification/Java.vo                                         |  0m00.90s |  519208 ko || -0m00.05s ||       -44 ko |   -5.55% |         -0.00%
 0m00.83s |  580632 ko | Bedrock/Field/Common/Tactics.vo                                 |  0m00.76s |  580504 ko || +0m00.06s ||       128 ko |   +9.21% |         +0.02%
 0m00.83s |  522380 ko | Bedrock/Field/Stringification/LoadStoreListVarData.vo           |  0m00.72s |  522256 ko || +0m00.10s ||       124 ko |  +15.27% |         +0.02%
 0m00.81s |  524152 ko | Bedrock/Field/Translation/Proofs/Equivalence.vo                 |  0m00.82s |  523904 ko || -0m00.00s ||       248 ko |   -1.21% |         +0.04%
 0m00.80s |  524288 ko | Bedrock/Field/Translation/LoadStoreList.vo                      |  0m00.75s |  524268 ko || +0m00.05s ||        20 ko |   +6.66% |         +0.00%
 0m00.78s |  529496 ko | Bedrock/Field/Stringification/FlattenVarData.vo                 |  0m00.77s |  529492 ko || +0m00.01s ||         4 ko |   +1.29% |         +0.00%
 0m00.76s |  498324 ko | Language/APINotations.vo                                        |  0m00.78s |  498232 ko || -0m00.02s ||        92 ko |   -2.56% |         +0.01%
 0m00.75s |  490512 ko | Bedrock/ScalarField/Interface/Compilation.vo                    |  0m00.76s |  490564 ko || -0m00.01s ||       -52 ko |   -1.31% |         -0.01%
 0m00.75s |  495092 ko | MiscCompilerPassesProofsExtra.vo                                |  0m00.69s |  494996 ko || +0m00.06s ||        96 ko |   +8.69% |         +0.01%
 0m00.74s |  523384 ko | Bedrock/Field/Common/Types.vo                                   |  0m00.70s |  523416 ko || +0m00.04s ||       -32 ko |   +5.71% |         -0.00%
 0m00.74s |  546124 ko | Rewriter/All.vo                                                 |  0m00.73s |  546132 ko || +0m00.01s ||        -8 ko |   +1.36% |         -0.00%
 0m00.73s |  454756 ko | Arithmetic/BarrettReduction/Wikipedia.vo                        |  0m00.76s |  454916 ko || -0m00.03s ||      -160 ko |   -3.94% |         -0.03%
 0m00.73s |  522316 ko | Bedrock/Field/Translation/Proofs/VarnameSet.vo                  |  0m00.69s |  522172 ko || +0m00.04s ||       144 ko |   +5.79% |         +0.02%
 0m00.73s |  460424 ko | Util/NumTheoryUtil.vo                                           |  0m00.64s |  460604 ko || +0m00.08s ||      -180 ko |  +14.06% |         -0.03%
 0m00.69s |  522344 ko | Bedrock/Field/Translation/Flatten.vo                            |  0m00.67s |  522400 ko || +0m00.01s ||       -56 ko |   +2.98% |         -0.01%
 0m00.69s |  435656 ko | Rewriter/Rules.vo                                               |  0m00.74s |  435660 ko || -0m00.05s ||        -4 ko |   -6.75% |         -0.00%
 0m00.66s |  511652 ko | Bedrock/Field/Common/Arrays/MakeListLengths.vo                  |  0m00.69s |  511520 ko || -0m00.02s ||       132 ko |   -4.34% |         +0.02%
 0m00.66s |  497080 ko | Language/WfExtra.vo                                             |  0m00.64s |  497008 ko || +0m00.02s ||        72 ko |   +3.12% |         +0.01%
 0m00.65s |  494840 ko | Language/UnderLetsProofsExtra.vo                                |  0m00.64s |  495132 ko || +0m00.01s ||      -292 ko |   +1.56% |         -0.05%
 0m00.65s |  497424 ko | Rewriter/AllTacticsExtra.vo                                     |  0m00.60s |  497524 ko || +0m00.05s ||      -100 ko |   +8.33% |         -0.02%
 0m00.64s |  499412 ko | AbstractInterpretation/WfExtra.vo                               |  0m00.71s |  499360 ko || -0m00.06s ||        52 ko |   -9.85% |         +0.01%
 0m00.64s |  509520 ko | PushButtonSynthesis/ReificationCache.vo                         |  0m00.67s |  509416 ko || -0m00.03s ||       104 ko |   -4.47% |         +0.02%
 0m00.63s |  490496 ko | Language/API.vo                                                 |  0m00.66s |  490452 ko || -0m00.03s ||        44 ko |   -4.54% |         +0.00%
 0m00.61s |  437524 ko | Util/ZRange/OperationsBounds.vo                                 |  0m00.58s |  437376 ko || +0m00.03s ||       148 ko |   +5.17% |         +0.03%
 0m00.60s |  470064 ko | Util/QUtil.vo                                                   |  0m00.46s |  470032 ko || +0m00.13s ||        32 ko |  +30.43% |         +0.00%
 0m00.59s |  454756 ko | Util/ZUtil/Stabilization.vo                                     |  0m00.56s |  454792 ko || +0m00.02s ||       -36 ko |   +5.35% |         -0.00%
 0m00.58s |  431820 ko | ArithmeticCPS/WordByWordMontgomery.vo                           |  0m00.56s |  431584 ko || +0m00.01s ||       236 ko |   +3.57% |         +0.05%
 0m00.56s |  429368 ko | ArithmeticCPS/Freeze.vo                                         |  0m00.54s |  429284 ko || +0m00.02s ||        84 ko |   +3.70% |         +0.01%
 0m00.56s |  421348 ko | Util/CPSUtil.vo                                                 |  0m00.62s |  421360 ko || -0m00.05s ||       -12 ko |   -9.67% |         -0.00%
 0m00.55s |  460104 ko | Util/ZUtil/CC.vo                                                |  0m00.55s |  460032 ko || +0m00.00s ||        72 ko |   +0.00% |         +0.01%
 0m00.54s |  443144 ko | Assembly/Equality.vo                                            |  0m00.60s |  443240 ko || -0m00.05s ||       -96 ko |   -9.99% |         -0.02%
 0m00.53s |  434684 ko | Bedrock/Specs/Field.vo                                          |  0m00.53s |  434564 ko || +0m00.00s ||       120 ko |   +0.00% |         +0.02%
 0m00.52s |  413800 ko | Bedrock/Group/Point.vo                                          |  0m00.48s |  413664 ko || +0m00.04s ||       136 ko |   +8.33% |         +0.03%
 0m00.52s |  433812 ko | Bedrock/Specs/Group.vo                                          |  0m00.46s |  433808 ko || +0m00.06s ||         4 ko |  +13.04% |         +0.00%
 0m00.51s |  454632 ko | ArithmeticCPS/ModOps.vo                                         |  0m00.45s |  454436 ko || +0m00.06s ||       196 ko |  +13.33% |         +0.04%
 0m00.51s |  449912 ko | Util/Decidable/Decidable2Bool.vo                                |  0m00.47s |  449908 ko || +0m00.04s ||         4 ko |   +8.51% |         +0.00%
 0m00.47s |  440884 ko | Bedrock/Specs/ScalarField.vo                                    |  0m00.60s |  440816 ko || -0m00.13s ||        68 ko |  -21.66% |         +0.01%
 0m00.45s |  440700 ko | ArithmeticCPS/BaseConversion.vo                                 |  0m00.41s |  440240 ko || +0m00.04s ||       460 ko |   +9.75% |         +0.10%
 0m00.45s |  450104 ko | ArithmeticCPS/Saturated.vo                                      |  0m00.46s |  450096 ko || -0m00.01s ||         8 ko |   -2.17% |         +0.00%
 0m00.44s |  447832 ko | ArithmeticCPS/Core.vo                                           |  0m00.41s |  447832 ko || +0m00.03s ||         0 ko |   +7.31% |         +0.00%
 0m00.43s |  445164 ko | Util/ZUtil/Ltz.vo                                               |  0m00.38s |  445268 ko || +0m00.04s ||      -104 ko |  +13.15% |         -0.02%
 0m00.42s |  453284 ko | Util/ZUtil/EquivModulo.vo                                       |  0m00.38s |  453060 ko || +0m00.03s ||       224 ko |  +10.52% |         +0.04%
 0m00.41s |  420456 ko | Util/HList.vo                                                   |  0m00.44s |  420108 ko || -0m00.03s ||       348 ko |   -6.81% |         +0.08%
 0m00.41s |  448896 ko | Util/ZUtil/Log2.vo                                              |  0m00.46s |  448852 ko || -0m00.05s ||        44 ko |  -10.86% |         +0.00%
 0m00.40s |  457528 ko | Util/ZUtil/SignBit.vo                                           |  0m00.41s |  457556 ko || -0m00.00s ||       -28 ko |   -2.43% |         -0.00%
 0m00.39s |  456680 ko | Util/ZUtil/Divide.vo                                            |  0m00.39s |  456560 ko || +0m00.00s ||       120 ko |   +0.00% |         +0.02%
 0m00.38s |  413784 ko | Language/IdentifierParameters.vo                                |  0m00.35s |  413788 ko || +0m00.03s ||        -4 ko |   +8.57% |         -0.00%
 0m00.38s |  453164 ko | Util/ZUtil/Land.vo                                              |  0m00.40s |  452980 ko || -0m00.02s ||       184 ko |   -5.00% |         +0.04%
 0m00.37s |  424472 ko | Util/ZRange.vo                                                  |  0m00.40s |  424412 ko || -0m00.03s ||        60 ko |   -7.50% |         +0.01%
 0m00.36s |  396768 ko | Language/PreExtra.vo                                            |  0m00.32s |  396744 ko || +0m00.03s ||        24 ko |  +12.49% |         +0.00%
 0m00.35s |  405464 ko | Rewriter/TestRules.vo                                           |  0m00.37s |  405440 ko || -0m00.02s ||        24 ko |   -5.40% |         +0.00%
 0m00.35s |  365772 ko | Rewriter/TestRulesProofs.vo                                     |  0m00.35s |  365476 ko || +0m00.00s ||       296 ko |   +0.00% |         +0.08%
 0m00.34s |  424696 ko | Util/ZBounded.vo                                                |  0m00.45s |  424692 ko || -0m00.10s ||         4 ko |  -24.44% |         +0.00%
 0m00.32s |  429692 ko | Arithmetic/ModularArithmeticPre.vo                              |  0m00.36s |  429536 ko || -0m00.03s ||       156 ko |  -11.11% |         +0.03%
 0m00.32s |  324964 ko | Util/ZUtil/Tactics/SimplifyFractionsLe.vo                       |  0m00.27s |  324844 ko || +0m00.04s ||       120 ko |  +18.51% |         +0.03%
 0m00.31s |  331912 ko | Arithmetic/MontgomeryReduction/Definition.vo                    |  0m00.26s |  331780 ko || +0m00.04s ||       132 ko |  +19.23% |         +0.03%
 0m00.30s |  335636 ko | Spec/ModularArithmetic.vo                                       |  0m00.32s |  335728 ko || -0m00.02s ||       -92 ko |   -6.25% |         -0.02%
 0m00.30s |  359368 ko | Util/ZUtil/Lor.vo                                               |  0m00.29s |  359240 ko || +0m00.01s ||       128 ko |   +3.44% |         +0.03%
 0m00.30s |  320064 ko | Util/ZUtil/Tactics.vo                                           |  0m00.27s |  320140 ko || +0m00.02s ||       -76 ko |  +11.11% |         -0.02%
 0m00.30s |  355936 ko | Util/ZUtil/Tactics/SolveRange.vo                                |  0m00.34s |  355864 ko || -0m00.04s ||        72 ko |  -11.76% |         +0.02%
 0m00.30s |  352844 ko | Util/ZUtil/Tactics/SolveTestbit.vo                              |  0m00.31s |  353120 ko || -0m00.01s ||      -276 ko |   -3.22% |         -0.07%
 0m00.29s |  347632 ko | Util/ZUtil/Tactics/Ztestbit.vo                                  |  0m00.26s |  347400 ko || +0m00.02s ||       232 ko |  +11.53% |         +0.06%
 0m00.27s |  322968 ko | Util/IdfunWithAlt.vo                                            |  0m00.23s |  322844 ko || +0m00.04s ||       124 ko |  +17.39% |         +0.03%
 0m00.27s |  332116 ko | Util/ListUtil/Permutation.vo                                    |    N/A    |    N/A     || +0m00.27s ||    332116 ko |        ∞ |              ∞
 0m00.26s |  369152 ko | Util/ZUtil.vo                                                   |  0m00.30s |  368620 ko || -0m00.03s ||       532 ko |  -13.33% |         +0.14%
 0m00.25s |  368968 ko | Util/ZRange/Operations.vo                                       |  0m00.32s |  368944 ko || -0m00.07s ||        24 ko |  -21.87% |         +0.00%
 0m00.25s |  321652 ko | Util/ZRange/Show.vo                                             |  0m00.22s |  321460 ko || +0m00.03s ||       192 ko |  +13.63% |         +0.05%
 0m00.24s |  291664 ko | Util/SideConditions/Autosolve.vo                                |  0m00.30s |  291564 ko || -0m00.06s ||       100 ko |  -20.00% |         +0.03%
 0m00.23s |  297052 ko | Util/SideConditions/ModInvPackage.vo                            |  0m00.22s |  296832 ko || +0m00.01s ||       220 ko |   +4.54% |         +0.07%
 0m00.23s |  321912 ko | Util/ZUtil/Tactics/ZeroBounds.vo                                |  0m00.26s |  321496 ko || -0m00.03s ||       416 ko |  -11.53% |         +0.12%
 0m00.21s |  339904 ko | Util/ZUtil/Tactics/RewriteModSmall.vo                           |  0m00.25s |  340112 ko || -0m00.04s ||      -208 ko |  -16.00% |         -0.06%
 0m00.20s |  268368 ko | Util/ZUtil/Hints.vo                                             |  0m00.21s |  268548 ko || -0m00.00s ||      -180 ko |   -4.76% |         -0.06%
 0m00.20s |  267548 ko | Util/ZUtil/Hints/ZArith.vo                                      |  0m00.23s |  267636 ko || -0m00.03s ||       -88 ko |  -13.04% |         -0.03%
 0m00.18s |  313444 ko | Util/NUtil/Testbit.vo                                           |    N/A    |    N/A     || +0m00.18s ||    313444 ko |        ∞ |              ∞
 0m00.12s |  182880 ko | Util/ListUtil/PermutationCompat.vo                              |    N/A    |    N/A     || +0m00.12s ||    182880 ko |        ∞ |              ∞
 0m00.04s |   82988 ko | Util/Bool/LeCompat.vo                                           |  0m00.05s |   74072 ko || -0m00.01s ||      8916 ko |  -20.00% |        +12.03%

```
</p>
</details>

_CoqProject.in

@@ -301,6 +301,8 @@ src/Util/ListUtil/Forall.v
 src/Util/ListUtil/ForallIn.v
 src/Util/ListUtil/IndexOf.v
 src/Util/ListUtil/NthExt.v
+src/Util/ListUtil/Permutation.v
+src/Util/ListUtil/PermutationCompat.v
 src/Util/ListUtil/SetoidList.v
 src/Util/Logic/Exists.v
 src/Util/Logic/ExistsEqAnd.v
@@ -314,6 +316,7 @@ src/Util/MSets/Iso.v
 src/Util/MSets/Show.v
 src/Util/MSets/Sum.v
 src/Util/NUtil/Sorting.v
+src/Util/NUtil/Testbit.v
 src/Util/NUtil/WithoutReferenceToZ.v
 src/Util/SideConditions/Autosolve.v
 src/Util/SideConditions/CorePackages.v

src/Util/Bool/LeCompat.v

@@ -4,6 +4,14 @@ Module Export Coq.
   Module Export Bool.
     Module Bool.
       Definition le (b1 b2 : bool) := if b1 then b2 = true else True.
+      Lemma le_implb : forall b1 b2, le b1 b2 <-> implb b1 b2 = true.
+      Proof.
+        destr_bool; intuition.
+      Qed.
+      Lemma implb_true_r : forall b:bool, implb b true = true.
+      Proof.
+        destr_bool.
+      Qed.
     End Bool.
   End Bool.
 End Coq.

src/Util/ListUtil/Permutation.v

@@ -0,0 +1,65 @@
+Require Import Coq.NArith.NArith.
+Require Import Coq.Arith.Arith.
+Require Import Coq.ZArith.ZArith.
+Require Import Coq.Lists.List.
+Require Import Coq.Sorting.Permutation.
+Require Import Coq.Setoids.Setoid.
+Require Import Coq.Classes.Morphisms.
+Require Import Crypto.Util.Tactics.BreakMatch.
+Import ListNotations.
+
+Lemma Permutation_partition {A} (l : list A) f :
+    Permutation.Permutation l (fst (partition f l) ++ snd (partition f l)).
+Proof using Type.
+  induction l; cbn; break_match; cbn in *; eauto.
+  etransitivity. econstructor. eassumption.
+  eapply Permutation.Permutation_middle.
+Qed.
+
+Global Instance fold_right_Proper_commutative_associative_Permutation {A op}
+       (Hcomm : forall x y, op x y = op y x)
+       (Hassoc : forall x y z, op x (op y z) = op (op x y) z)
+  : Proper (eq ==> @Permutation A ==> eq) (fold_right op) | 1000.
+Proof using Type.
+  intros init init' <- xs ys; induction 1; cbn;
+    rewrite ?Hassoc;
+    repeat match goal with
+           | [ |- context[op ?x ?y] ]
+             => lazymatch goal with
+                | [ |- context[op y x] ]
+                  => rewrite (Hcomm x y)
+                end
+           end;
+    try reflexivity;
+    try now repeat match goal with H : _ |- _ => rewrite H; clear H end.
+Qed.
+
+Module Nat.
+  Global Instance fold_right_Proper_Permutation_add
+  : Proper (eq ==> @Permutation _ ==> eq) (fold_right Nat.add) | 100.
+  Proof using Type. apply fold_right_Proper_commutative_associative_Permutation; [ hnf; apply Nat.add_comm | hnf; apply Nat.add_assoc ]. Qed.
+
+  Global Instance fold_right_Proper_Permutation_mul
+  : Proper (eq ==> @Permutation _ ==> eq) (fold_right Nat.mul) | 100.
+  Proof using Type. apply fold_right_Proper_commutative_associative_Permutation; [ hnf; apply Nat.mul_comm | hnf; apply Nat.mul_assoc ]. Qed.
+End Nat.
+
+Module N.
+  Global Instance fold_right_Proper_Permutation_add
+  : Proper (eq ==> @Permutation _ ==> eq) (fold_right N.add) | 100.
+  Proof using Type. apply fold_right_Proper_commutative_associative_Permutation; [ hnf; apply N.add_comm | hnf; apply N.add_assoc ]. Qed.
+
+  Global Instance fold_right_Proper_Permutation_mul
+  : Proper (eq ==> @Permutation _ ==> eq) (fold_right N.mul) | 100.
+  Proof using Type. apply fold_right_Proper_commutative_associative_Permutation; [ hnf; apply N.mul_comm | hnf; apply N.mul_assoc ]. Qed.
+End N.
+
+Module Z.
+  Global Instance fold_right_Proper_Permutation_add
+  : Proper (eq ==> @Permutation _ ==> eq) (fold_right Z.add) | 100.
+  Proof using Type. apply fold_right_Proper_commutative_associative_Permutation; [ hnf; apply Z.add_comm | hnf; apply Z.add_assoc ]. Qed.
+
+  Global Instance fold_right_Proper_Permutation_mul
+  : Proper (eq ==> @Permutation _ ==> eq) (fold_right Z.mul) | 100.
+  Proof using Type. apply fold_right_Proper_commutative_associative_Permutation; [ hnf; apply Z.mul_comm | hnf; apply Z.mul_assoc ]. Qed.
+End Z.

src/Util/ListUtil/PermutationCompat.v

@@ -0,0 +1,45 @@
+Require Import Coq.Lists.List.
+Require Import Coq.Sorting.Permutation.
+Import List Setoid Compare_dec Morphisms FinFun PeanoNat Permutation.
+Import ListNotations.
+Local Set Implicit Arguments.
+
+(** From Coq's Coq.Sorting.Permutation file on newer versions of Coq than 8.11 *)
+Module Export Coq.
+Module Export Sorting.
+Module Permutation.
+Export Coq.Sorting.Permutation.
+
+Section Permutation_properties.
+
+Variable A B:Type.
+
+Implicit Types a b : A.
+Implicit Types l m : list A.
+
+(** TODO: Remove this when be bump the minimum version to Coq 8.12 *)
+Local Hint Resolve perm_swap perm_trans : core.
+Lemma Permutation_Forall2 (P : A -> B -> Prop) :
+ forall l1 l1' (l2 : list B), Permutation l1 l1' -> Forall2 P l1 l2 ->
+ exists l2' : list B, Permutation l2 l2' /\ Forall2 P l1' l2'.
+Proof using Type.
+  intros l1 l1' l2 HP.
+  revert l2; induction HP; intros l2 HF; inversion HF as [ | ? b ? ? HF1 HF2 ]; subst.
+  - now exists nil.
+  - apply IHHP in HF2 as [l2' [HP2 HF2]].
+    exists (b :: l2'); auto.
+  - inversion_clear HF2 as [ | ? b' ? l2' HF3 HF4 ].
+    exists (b' :: b :: l2'); auto.
+  - apply Permutation_nil in HP1; subst.
+    apply Permutation_nil in HP2; subst.
+    now exists nil.
+  - apply IHHP1 in HF as [l2' [HP2' HF2']].
+    apply IHHP2 in HF2' as [l2'' [HP2'' HF2'']].
+    exists l2''; split; auto.
+    now transitivity l2'.
+Qed.
+
+End Permutation_properties.
+End Permutation.
+End Sorting.
+End Coq.

src/Util/NUtil/Testbit.v

@@ -0,0 +1,24 @@
+Require Import Coq.micromega.Lia.
+Require Import Coq.NArith.NArith.
+
+Module N.
+  Lemma testbit_ones n i : N.testbit (N.ones n) i = N.ltb i n.
+  Proof using Type.
+    pose proof N.ones_spec_iff n i.
+    destruct (N.testbit _ _) eqn:? in*; destruct (N.ltb_spec i n); trivial.
+    { pose proof (proj1 H eq_refl); lia. }
+    { pose proof (proj2 H H0). inversion H1. }
+  Qed.
+
+  Lemma ones_min m n : N.ones (N.min m n) = N.land (N.ones m) (N.ones n).
+  Proof using Type.
+    eapply N.bits_inj_iff; intro i.
+    rewrite N.land_spec.
+    rewrite !N.testbit_ones.
+    destruct (N.ltb_spec0 i (N.min m n));
+      destruct (N.ltb_spec0 i m);
+      destruct (N.ltb_spec0 i n);
+      try reflexivity;
+      lia.
+  Qed.
+End N.