make elliptic curve proofs faster and split them into files

fix EdwardsMontgomery

try to speed up Weierstrass proof

--amend

Conflicts fixed by Jason Gross; timing diff added by Jason Gross

After     | File Name                                                              | Before    || Change
-----------------------------------------------------------------------------------------------------------
35m50.76s | Total                                                                  | 33m10.99s || +2m39.77s
-----------------------------------------------------------------------------------------------------------
2m07.08s  | MontgomeryXProofs                                                      |    N/A    || +2m07.07s
0m00.72s  | MontgomeryX                                                            | 1m39.97s  || -1m39.25s
12m47.53s | WeierstrassCurve/WeierstrassCurveTheorems                              | 11m33.56s || +1m13.97s
2m35.44s  | WeierstrassCurve/Projective                                            | 2m26.24s  || +0m09.19s
0m58.83s  | Specific/IntegrationTest                                               | 0m51.09s  || +0m07.73s
0m50.02s  | ModularArithmetic/ModularBaseSystemProofs                              | 0m42.63s  || +0m07.39s
0m24.81s  | EdDSARepChange                                                         | 0m18.72s  || +0m06.08s
0m26.89s  | CompleteEdwardsCurve/ExtendedCoordinates                               | 0m21.82s  || +0m05.07s
0m47.18s  | MontgomeryCurveTheorems                                                | 0m42.44s  || +0m04.74s
0m41.62s  | Spec/Ed25519                                                           | 0m37.32s  || +0m04.29s
0m18.06s  | Specific/NewBaseSystemTest                                             | 0m13.09s  || +0m04.96s
0m21.56s  | Reflection/Z/ArithmeticSimplifierWf                                    | 0m17.61s  || +0m03.94s
0m12.12s  | BoundedArithmetic/Double/Proofs/Multiply                               | 0m08.28s  || +0m03.83s
0m08.58s  | Reflection/InlineWf                                                    | 0m11.71s  || -0m03.13s
0m07.66s  | Algebra/Ring                                                           | 0m10.68s  || -0m03.01s
0m03.98s  | MontgomeryCurve                                                        |    N/A    || +0m03.98s
0m54.83s  | ModularArithmetic/Conversion                                           | 0m56.89s  || -0m02.06s
0m14.94s  | Algebra/Field                                                          | 0m12.60s  || +0m02.33s
0m11.18s  | BoundedArithmetic/ArchitectureToZLikeProofs                            | 0m09.07s  || +0m02.10s
0m08.33s  | Util/FixedWordSizesEquality                                            | 0m06.16s  || +0m02.16s
1m44.81s  | Test/Curve25519SpecTestVectors                                         | 1m46.63s  || -0m01.81s
0m27.28s  | Reflection/Named/MapCastWf                                             | 0m28.30s  || -0m01.01s
0m11.27s  | BoundedArithmetic/Double/Proofs/ShiftRightDoubleWordImmediate          | 0m09.99s  || +0m01.27s
0m08.72s  | MxDHRepChange                                                          | 0m09.76s  || -0m01.03s
0m04.74s  | BoundedArithmetic/InterfaceProofs                                      | 0m03.38s  || +0m01.36s
0m04.71s  | SaturatedBaseSystem                                                    | 0m03.70s  || +0m01.00s
0m03.85s  | ModularArithmetic/BarrettReduction/ZHandbook                           | 0m05.55s  || -0m01.69s
0m03.17s  | Reflection/LinearizeWf                                                 | 0m04.62s  || -0m01.45s
0m32.62s  | CompleteEdwardsCurve/CompleteEdwardsCurveTheorems                      | 0m33.15s  || -0m00.53s
0m28.02s  | ModularArithmetic/Pow2BaseProofs                                       | 0m28.89s  || -0m00.87s
0m27.30s  | Reflection/Z/Bounds/InterpretationLemmas                               | 0m26.88s  || +0m00.42s
0m21.01s  | Specific/GF25519                                                       | 0m20.88s  || +0m00.13s
0m19.39s  | Reflection/Named/ContextProperties/NameUtil                            | 0m20.12s  || -0m00.73s
0m18.99s  | Reflection/Named/ContextProperties/SmartMap                            | 0m19.90s  || -0m00.91s
0m15.32s  | Util/ZUtil                                                             | 0m16.14s  || -0m00.82s
0m14.19s  | Reflection/Z/ArithmeticSimplifierInterp                                | 0m13.86s  || +0m00.33s
0m13.42s  | Testbit                                                                | 0m12.97s  || +0m00.44s
0m12.74s  | Reflection/Named/MapCastInterp                                         | 0m12.39s  || +0m00.34s
0m10.83s  | ModularArithmetic/Montgomery/ZProofs                                   | 0m11.19s  || -0m00.35s
0m10.36s  | NewBaseSystem                                                          | 0m10.53s  || -0m00.16s
0m09.47s  | BoundedArithmetic/Double/Proofs/SpreadLeftImmediate                    | 0m10.15s  || -0m00.67s
0m09.22s  | Assembly/GF25519                                                       | 0m08.77s  || +0m00.45s
0m07.82s  | CompleteEdwardsCurve/Pre                                               | 0m07.86s  || -0m00.04s
0m07.60s  | BoundedArithmetic/Double/Proofs/RippleCarryAddSub                      | 0m08.19s  || -0m00.58s
0m07.08s  | Algebra/Field_test                                                     | 0m06.51s  || +0m00.57s
0m06.92s  | Specific/GF1305                                                        | 0m06.83s  || +0m00.08s
0m06.29s  | Specific/SC25519                                                       | 0m05.46s  || +0m00.83s
0m06.23s  | Bedrock/Word                                                           | 0m06.80s  || -0m00.56s
0m06.01s  | ModularArithmetic/ModularBaseSystemListProofs                          | 0m05.24s  || +0m00.76s
0m05.75s  | Reflection/Z/Syntax/Equality                                           | 0m05.64s  || +0m00.11s
0m05.66s  | Util/ListUtil                                                          | 0m05.91s  || -0m00.25s
0m05.63s  | Reflection/InlineCastWf                                                | 0m05.46s  || +0m00.16s
0m05.47s  | Experiments/GenericFieldPow                                            | 0m05.84s  || -0m00.37s
0m04.96s  | BaseSystemProofs                                                       | 0m03.98s  || +0m00.98s
0m04.93s  | Reflection/Named/CompileWf                                             | 0m05.12s  || -0m00.19s
0m04.38s  | ModularArithmetic/ModularArithmeticTheorems                            | 0m04.29s  || +0m00.08s
0m04.25s  | Spec/MontgomeryCurve                                                   | 0m04.22s  || +0m00.03s
0m04.19s  | Reflection/Named/CompileInterp                                         | 0m04.26s  || -0m00.06s
0m04.13s  | Specific/FancyMachine256/Montgomery                                    | 0m03.25s  || +0m00.87s
0m04.11s  | CompleteEdwardsCurve/EdwardsMontgomery                                 | 0m03.67s  || +0m00.44s
0m03.95s  | BoundedArithmetic/Double/Proofs/ShiftLeft                              | 0m04.14s  || -0m00.18s
0m03.86s  | ModularArithmetic/ZBoundedZ                                            | 0m03.16s  || +0m00.69s
0m03.85s  | Reflection/EtaWf                                                       | 0m03.74s  || +0m00.10s
0m03.79s  | BoundedArithmetic/Double/Proofs/ShiftRight                             | 0m03.53s  || +0m00.26s
0m03.76s  | Specific/FancyMachine256/Barrett                                       | 0m02.99s  || +0m00.76s
0m03.74s  | BoundedArithmetic/Double/Proofs/Decode                                 | 0m03.47s  || +0m00.27s
0m03.66s  | Reflection/TestCase                                                    | 0m03.34s  || +0m00.32s
0m03.40s  | Reflection/Z/Bounds/Relax                                              | 0m02.86s  || +0m00.54s
0m03.34s  | ModularArithmetic/BarrettReduction/ZBounded                            | 0m02.38s  || +0m00.96s
0m03.30s  | Reflection/Named/ContextProperties                                     | 0m02.60s  || +0m00.69s
0m02.94s  | ModularArithmetic/BarrettReduction/ZGeneralized                        | 0m03.86s  || -0m00.92s
0m02.82s  | Specific/FancyMachine256/Core                                          | 0m01.97s  || +0m00.84s
0m02.68s  | ModularArithmetic/ModularBaseSystemOpt                                 | 0m02.49s  || +0m00.18s
0m02.63s  | Reflection/InlineInterp                                                | 0m03.57s  || -0m00.94s
0m02.58s  | Assembly/State                                                         | 0m02.60s  || -0m00.02s
0m02.43s  | Reflection/Named/NameUtilProperties                                    | 0m02.36s  || +0m00.07s
0m02.43s  | ModularArithmetic/Montgomery/ZBounded                                  | 0m01.84s  || +0m00.59s
0m02.21s  | Reflection/WfProofs                                                    | 0m02.17s  || +0m00.04s
0m02.20s  | ModularArithmetic/PrimeFieldTheorems                                   | 0m02.06s  || +0m00.14s
0m02.12s  | WeierstrassCurve/Pre                                                   | 0m01.91s  || +0m00.21s
0m02.03s  | Util/WordUtil                                                          | 0m02.64s  || -0m00.61s
0m02.00s  | Assembly/Evaluables                                                    | 0m01.98s  || +0m00.02s
0m01.95s  | Reflection/Named/InterpretToPHOASWf                                    | 0m02.21s  || -0m00.26s
0m01.94s  | Reflection/WfReflective                                                | 0m02.74s  || -0m00.80s
0m01.84s  | Assembly/Bounds                                                        | 0m01.40s  || +0m00.44s
0m01.78s  | BoundedArithmetic/Double/Repeated/Proofs/Decode                        | 0m01.72s  || +0m00.06s
0m01.54s  | Assembly/Compile                                                       | 0m01.53s  || +0m00.01s
0m01.46s  | Assembly/WordizeUtil                                                   | 0m02.12s  || -0m00.66s
0m01.44s  | ModularArithmetic/BarrettReduction/Z                                   | 0m02.31s  || -0m00.87s
0m01.44s  | Reflection/Named/InterpretToPHOASInterp                                | 0m01.30s  || +0m00.13s
0m01.42s  | Util/NatUtil                                                           | 0m02.15s  || -0m00.73s
0m01.40s  | Reflection/Z/Bounds/Pipeline/Definition                                | 0m01.09s  || +0m00.30s
0m01.40s  | Util/Tuple                                                             | 0m01.45s  || -0m00.05s
0m01.36s  | ModularArithmetic/ExtendedBaseVector                                   | 0m01.84s  || -0m00.48s
0m01.36s  | Algebra/Group                                                          | 0m01.40s  || -0m00.03s
0m01.35s  | Assembly/Conversions                                                   | 0m01.21s  || +0m00.14s
0m01.34s  | BoundedArithmetic/X86ToZLikeProofs                                     | 0m00.83s  || +0m00.51s
0m01.34s  | Reflection/MapCastInterp                                               | 0m01.62s  || -0m00.28s
0m01.30s  | BoundedArithmetic/Double/Proofs/LoadImmediate                          | 0m01.25s  || +0m00.05s
0m01.20s  | BaseSystem                                                             | 0m01.56s  || -0m00.36s
0m01.19s  | BoundedArithmetic/Double/Proofs/BitwiseOr                              | 0m00.97s  || +0m00.21s
0m01.15s  | Reflection/InlineCastInterp                                            | 0m00.86s  || +0m00.28s
0m01.12s  | Reflection/SmartBoundInterp                                            | 0m01.04s  || +0m00.08s
0m01.06s  | Reflection/Relations                                                   | 0m01.05s  || +0m00.01s
0m01.04s  | ModularArithmetic/ModularBaseSystemList                                | 0m00.65s  || +0m00.39s
0m01.04s  | Assembly/PhoasCommon                                                   | 0m00.87s  || +0m00.17s
0m01.03s  | ModularArithmetic/ExtPow2BaseMulProofs                                 | 0m00.72s  || +0m00.31s
0m01.03s  | Assembly/HL                                                            | 0m01.18s  || -0m00.14s
0m01.02s  | Assembly/LL                                                            | 0m01.02s  || +0m00.00s
0m01.02s  | Assembly/Pipeline                                                      | 0m00.92s  || +0m00.09s
0m01.02s  | ModularArithmetic/ModularBaseSystem                                    | 0m00.76s  || +0m00.26s
0m01.01s  | Algebra/IntegralDomain                                                 | 0m01.12s  || -0m00.11s
0m01.00s  | Util/IterAssocOp                                                       | 0m00.78s  || +0m00.21s
0m00.96s  | Util/NumTheoryUtil                                                     | 0m01.34s  || -0m00.38s
0m00.95s  | Reflection/MapCastByDeBruijnInterp                                     | 0m00.83s  || +0m00.12s
0m00.95s  | ModularArithmetic/PseudoMersenneBaseParamProofs                        | 0m00.76s  || +0m00.18s
0m00.90s  | Reflection/Z/Bounds/Pipeline/ReflectiveTactics                         | 0m00.66s  || +0m00.24s
0m00.90s  | Reflection/SmartCastWf                                                 | 0m00.97s  || -0m00.06s
0m00.89s  | Encoding/ModularWordEncodingTheorems                                   | 0m00.71s  || +0m00.18s
0m00.88s  | Spec/CompleteEdwardsCurve                                              | 0m00.83s  || +0m00.05s
0m00.87s  | BoundedArithmetic/X86ToZLike                                           | 0m00.88s  || -0m00.01s
0m00.86s  | Spec/ModularWordEncoding                                               | 0m00.60s  || +0m00.26s
0m00.83s  | Reflection/Named/CompileProperties                                     | 0m00.88s  || -0m00.05s
0m00.83s  | Reflection/WfInversion                                                 | 0m00.82s  || +0m00.01s
0m00.82s  | Karatsuba                                                              | 0m01.20s  || -0m00.38s
0m00.82s  | WeierstrassCurve/Definitions                                           |    N/A    || +0m00.82s
0m00.81s  | BoundedArithmetic/Double/Proofs/SelectConditional                      | 0m00.80s  || +0m00.01s
0m00.80s  | Encoding/ModularWordEncodingPre                                        | 0m00.66s  || +0m00.14s
0m00.80s  | Reflection/MapCastByDeBruijnWf                                         | 0m00.91s  || -0m00.10s
0m00.78s  | BoundedArithmetic/Double/Core                                          | 0m00.69s  || +0m00.09s
0m00.78s  | BoundedArithmetic/Double/Repeated/Proofs/ShiftLeftRight                | 0m00.48s  || +0m00.30s
0m00.78s  | Assembly/QhasmEvalCommon                                               | 0m00.80s  || -0m00.02s
0m00.75s  | Util/PartiallyReifiedProp                                              | 0m00.73s  || +0m00.02s
0m00.74s  | Spec/EdDSA                                                             | 0m00.67s  || +0m00.06s
0m00.71s  | Reflection/BoundByCastInterp                                           | 0m00.77s  || -0m00.06s
0m00.71s  | Reflection/Z/Syntax/Util                                               | 0m00.80s  || -0m00.09s
0m00.71s  | Reflection/Z/Reify                                                     | 0m00.57s  || +0m00.14s
0m00.70s  | Util/NUtil                                                             | 0m00.52s  || +0m00.17s
0m00.70s  | Reflection/Z/CNotations                                                | 0m00.56s  || +0m00.13s
0m00.70s  | Spec/WeierstrassCurve                                                  | 0m00.84s  || -0m00.14s
0m00.69s  | Assembly/StringConversion                                              | 0m00.50s  || +0m00.18s
0m00.69s  | Reflection/Z/JavaNotations                                             | 0m00.54s  || +0m00.14s
0m00.68s  | BoundedArithmetic/Double/Repeated/Proofs/LoadImmediate                 | 0m00.47s  || +0m00.21s
0m00.67s  | Reflection/MultiSizeTest                                               | 0m00.70s  || -0m00.02s
0m00.67s  | BoundedArithmetic/Double/Repeated/Proofs/Multiply                      | 0m00.68s  || -0m00.01s
0m00.66s  | BoundedArithmetic/Double/Repeated/Proofs/SelectConditional             | 0m00.46s  || +0m00.20s
0m00.65s  | BoundedArithmetic/Double/Repeated/Proofs/BitwiseOr                     | 0m00.53s  || +0m00.12s
0m00.64s  | BoundedArithmetic/Double/Repeated/Proofs/RippleCarryAddSub             | 0m00.49s  || +0m00.15s
0m00.62s  | Reflection/Z/Bounds/Pipeline/Glue                                      | 0m00.69s  || -0m00.06s
0m00.62s  | Reflection/Z/Bounds/MapCastByDeBruijn                                  | 0m00.57s  || +0m00.05s
0m00.62s  | Reflection/Z/Bounds/Pipeline                                           | 0m00.51s  || +0m00.10s
0m00.62s  | BoundedArithmetic/Double/Repeated/Core                                 | 0m00.77s  || -0m00.15s
0m00.61s  | BoundedArithmetic/Double/Proofs/ShiftLeftRightTactic                   | 0m00.42s  || +0m00.19s
0m00.60s  | BoundedArithmetic/Interface                                            | 0m00.78s  || -0m00.18s
0m00.60s  | Reflection/Z/MapCastByDeBruijnWf                                       | 0m00.46s  || +0m00.13s
0m00.57s  | Reflection/Named/WfInterp                                              | 0m00.60s  || -0m00.03s
0m00.57s  | Reflection/Named/DeadCodeElimination                                   | 0m00.45s  || +0m00.11s
0m00.56s  | Util/AdditionChainExponentiation                                       | 0m00.48s  || +0m00.08s
0m00.55s  | Reflection/Named/PositiveContext/DefaultsProperties                    | 0m00.58s  || -0m00.02s
0m00.54s  | Reflection/InterpByIsoProofs                                           | 0m00.80s  || -0m00.26s
0m00.54s  | BoundedArithmetic/ArchitectureToZLike                                  | 0m00.70s  || -0m00.15s
0m00.54s  | BoundedArithmetic/Double/Repeated/Proofs/ShiftRightDoubleWordImmediate | 0m00.47s  || +0m00.07s
0m00.54s  | Reflection/Z/InlineWf                                                  | 0m00.57s  || -0m00.02s
0m00.54s  | Reflection/Named/FMapContext                                           | 0m00.73s  || -0m00.18s
0m00.54s  | BoundedArithmetic/StripCF                                              | 0m00.48s  || +0m00.06s
0m00.54s  | Reflection/Z/MapCastByDeBruijn                                         | 0m00.58s  || -0m00.03s
0m00.53s  | Reflection/Z/MapCastByDeBruijnInterp                                   | 0m00.66s  || -0m00.13s
0m00.53s  | Reflection/Z/FoldTypes                                                 | 0m00.56s  || -0m00.03s
0m00.53s  | Reflection/Z/Bounds/MapCastByDeBruijnInterp                            | 0m00.40s  || +0m00.13s
0m00.53s  | Reflection/Z/Bounds/MapCastByDeBruijnWf                                | 0m00.40s  || +0m00.13s
0m00.53s  | Reflection/WfReflectiveGen                                             | 0m00.56s  || -0m00.03s
0m00.52s  | Reflection/Z/HexNotationConstants                                      | 0m00.53s  || -0m00.01s
0m00.52s  | Util/CPSUtil                                                           | 0m00.49s  || +0m00.03s
0m00.52s  | Reflection/Z/Inline                                                    | 0m00.58s  || -0m00.05s
0m00.52s  | ModularArithmetic/Pre                                                  | 0m00.42s  || +0m00.10s
0m00.52s  | Reflection/Z/Bounds/Pipeline/OutputType                                | 0m00.35s  || +0m00.17s
0m00.50s  | Util/Decidable                                                         | 0m00.51s  || -0m00.01s
0m00.50s  | Reflection/InterpWf                                                    | 0m00.46s  || +0m00.03s
0m00.49s  | Reflection/Z/ArithmeticSimplifier                                      | 0m00.65s  || -0m00.16s
0m00.49s  | Reflection/SmartBoundWf                                                | 0m00.56s  || -0m00.07s
0m00.48s  | Reflection/Named/PositiveContext                                       | 0m00.47s  || +0m00.01s
0m00.48s  | Reflection/Named/PositiveContext/Defaults                              | 0m00.60s  || -0m00.12s
0m00.48s  | Reflection/MapCastByDeBruijn                                           | 0m00.44s  || +0m00.03s
0m00.48s  | Spec/ModularArithmetic                                                 | 0m00.44s  || +0m00.03s
0m00.48s  | Reflection/InputSyntax                                                 | 0m00.59s  || -0m00.10s
0m00.48s  | Reflection/InterpWfRel                                                 | 0m00.50s  || -0m00.02s
0m00.47s  | ModularArithmetic/Pow2Base                                             | 0m00.56s  || -0m00.09s
0m00.46s  | BoundedArithmetic/Eta                                                  | 0m00.39s  || +0m00.07s
0m00.45s  | Reflection/Z/Syntax                                                    | 0m00.50s  || -0m00.04s
0m00.44s  | Reflection/Z/Bounds/Interpretation                                     | 0m00.60s  || -0m00.15s
0m00.44s  | Assembly/Qhasm                                                         | 0m00.72s  || -0m00.27s
0m00.44s  | Util/HList                                                             | 0m00.47s  || -0m00.02s
0m00.44s  | Reflection/Named/RegisterAssign                                        | 0m00.40s  || +0m00.03s
0m00.42s  | ModularArithmetic/ModularBaseSystemListZOperations                     | 0m00.38s  || +0m00.03s
0m00.42s  | ModularArithmetic/ModularBaseSystemWord                                | 0m00.37s  || +0m00.04s
0m00.42s  | ModularArithmetic/ZBounded                                             | 0m00.64s  || -0m00.22s
0m00.41s  | Reflection/Z/InlineInterp                                              | 0m00.58s  || -0m00.17s
0m00.41s  | ModularArithmetic/PseudoMersenneBaseParams                             | 0m00.55s  || -0m00.14s
0m00.40s  | Assembly/QhasmUtil                                                     | 0m00.42s  || -0m00.01s
0m00.40s  | Util/ZRange                                                            | 0m00.43s  || -0m00.02s
0m00.40s  | ModularArithmetic/ModularBaseSystemListZOperationsProofs               | 0m00.59s  || -0m00.18s
0m00.39s  | Util/BoundedWord                                                       | 0m00.40s  || -0m00.01s
0m00.38s  | Reflection/Named/Wf                                                    | 0m00.38s  || +0m00.00s
0m00.38s  | Reflection/FilterLive                                                  | 0m00.32s  || +0m00.06s
0m00.38s  | Reflection/Named/EstablishLiveness                                     | 0m00.34s  || +0m00.03s
0m00.38s  | Reflection/MultiSizeTest2                                              | 0m00.44s  || -0m00.06s
0m00.38s  | Reflection/Tuple                                                       | 0m00.40s  || -0m00.02s
0m00.38s  | ModularArithmetic/Montgomery/Z                                         | 0m00.58s  || -0m00.19s
0m00.37s  | Reflection/Named/ContextDefinitions                                    | 0m00.34s  || +0m00.02s
0m00.37s  | Reflection/Reify                                                       | 0m00.51s  || -0m00.14s
0m00.37s  | Reflection/Named/ContextProperties/Tactics                             | 0m00.43s  || -0m00.06s
0m00.36s  | Tactics/Algebra_syntax/Nsatz                                           | 0m00.58s  || -0m00.21s
0m00.36s  | Reflection/Named/Syntax                                                | 0m00.38s  || -0m00.02s
0m00.36s  | Reflection/Named/InterpretToPHOAS                                      | 0m00.46s  || -0m00.10s
0m00.36s  | Reflection/Named/Compile                                               | 0m00.35s  || +0m00.01s
0m00.35s  | Util/Factorize                                                         | 0m00.46s  || -0m00.11s
0m00.34s  | Reflection/Named/MapCast                                               | 0m00.33s  || +0m00.01s
0m00.34s  | Reflection/Named/IdContext                                             | 0m00.35s  || -0m00.00s
0m00.34s  | Reflection/Named/SmartMap                                              | 0m00.35s  || -0m00.00s
0m00.34s  | Reflection/Z/BinaryNotationConstants                                   | 0m00.53s  || -0m00.19s
0m00.33s  | Reflection/Z/OpInversion                                               | 0m00.44s  || -0m00.10s
0m00.32s  | Algebra/ScalarMult                                                     | 0m00.27s  || +0m00.04s
0m00.32s  | Reflection/MapCastWf                                                   | 0m00.50s  || -0m00.18s
0m00.32s  | Util/FixedWordSizes                                                    | 0m00.34s  || -0m00.02s
0m00.32s  | Reflection/Named/ContextOn                                             | 0m00.36s  || -0m00.03s
0m00.31s  | Assembly/QhasmCommon                                                   | 0m00.29s  || +0m00.02s
0m00.31s  | Reflection/ExprInversion                                               | 0m00.27s  || +0m00.03s
0m00.28s  | Bedrock/Nomega                                                         | 0m00.40s  || -0m00.12s
0m00.28s  | Reflection/SmartMap                                                    | 0m00.22s  || +0m00.06s
0m00.26s  | Reflection/Equality                                                    | 0m00.26s  || +0m00.00s
0m00.26s  | Util/Sum                                                               | 0m00.24s  || +0m00.02s
0m00.26s  | Algebra/Monoid                                                         | 0m00.26s  || +0m00.00s
0m00.26s  | Reflection/LinearizeInterp                                             | 0m00.24s  || +0m00.02s
0m00.26s  | Algebra                                                                | 0m00.30s  || -0m00.03s
0m00.24s  | Reflection/EtaInterp                                                   | 0m00.20s  || +0m00.03s
0m00.23s  | Util/CaseUtil                                                          | 0m00.33s  || -0m00.10s
0m00.21s  | Spec/MxDH                                                              | 0m00.27s  || -0m00.06s
0m00.19s  | Util/LetInMonad                                                        | 0m00.28s  || -0m00.09s
0m00.19s  | Reflection/CommonSubexpressionElimination                              | 0m00.18s  || +0m00.01s
0m00.18s  | Reflection/InterpProofs                                                | 0m00.19s  || -0m00.01s
0m00.18s  | Util/Option                                                            | 0m00.12s  || +0m00.06s
0m00.17s  | Reflection/BoundByCastWf                                               | 0m00.21s  || -0m00.03s
0m00.16s  | Experiments/ExtrHaskellNats                                            | 0m00.27s  || -0m00.11s
0m00.14s  | Reflection/RewriterWf                                                  | 0m00.18s  || -0m00.03s
0m00.13s  | Reflection/Conversion                                                  | 0m00.08s  || +0m00.05s
0m00.13s  | Reflection/Wf                                                          | 0m00.15s  || -0m00.01s
0m00.12s  | Reflection/Named/NameUtil                                              | 0m00.14s  || -0m00.02s
0m00.11s  | Reflection/TypeInversion                                               | 0m00.07s  || +0m00.03s
0m00.10s  | Util/Sigma                                                             | 0m00.13s  || -0m00.03s
0m00.10s  | Reflection/RewriterInterp                                              | 0m00.10s  || +0m00.00s
0m00.09s  | Util/Relations                                                         | 0m00.10s  || -0m00.01s
0m00.08s  | Util/Prod                                                              | 0m00.13s  || -0m00.05s
0m00.08s  | Util/PointedProp                                                       | 0m00.13s  || -0m00.05s
0m00.07s  | Reflection/InlineCast                                                  | 0m00.04s  || +0m00.03s
0m00.06s  | Reflection/BoundByCast                                                 | 0m00.04s  || +0m00.01s
0m00.06s  | Util/Equality                                                          | 0m00.08s  || -0m00.02s
0m00.05s  | Reflection/SmartCastInterp                                             | 0m00.04s  || +0m00.01s
0m00.05s  | Reflection/Inline                                                      | 0m00.06s  || -0m00.00s
0m00.05s  | Reflection/Syntax                                                      | 0m00.08s  || -0m00.03s
0m00.05s  | Reflection/FoldTypes                                                   | 0m00.04s  || +0m00.01s
0m00.05s  | Reflection/SmartBound                                                  | 0m00.08s  || -0m00.03s
0m00.05s  | Reflection/MapCast                                                     | 0m00.09s  || -0m00.03s
0m00.05s  | Util/Tactics                                                           | 0m00.04s  || +0m00.01s
0m00.04s  | Reflection/CountLets                                                   | 0m00.05s  || -0m00.01s
0m00.04s  | Util/HProp                                                             | 0m00.06s  || -0m00.01s
0m00.04s  | Util/Bool                                                              | 0m00.02s  || +0m00.02s
0m00.04s  | Reflection/TypeUtil                                                    | 0m00.05s  || -0m00.01s
0m00.04s  | Util/Tactics/BreakMatch                                                | 0m00.04s  || +0m00.00s
0m00.04s  | Reflection/RenameBinders                                               | 0m00.03s  || +0m00.01s
0m00.04s  | Reflection/InterpByIso                                                 | 0m00.04s  || +0m00.00s
0m00.04s  | Util/Sumbool                                                           | 0m00.05s  || -0m00.01s
0m00.04s  | Reflection/Linearize                                                   | 0m00.04s  || +0m00.00s
0m00.04s  | Reflection/Map                                                         | 0m00.05s  || -0m00.01s
0m00.04s  | Util/Tower                                                             | 0m00.04s  || +0m00.00s
0m00.04s  | Reflection/SmartCast                                                   | 0m00.03s  || +0m00.01s
0m00.04s  | Util/AutoRewrite                                                       | 0m00.04s  || +0m00.00s
0m00.04s  | Reflection/Eta                                                         | 0m00.05s  || -0m00.01s
0m00.03s  | Util/Tactics/RewriteHyp                                                | 0m00.03s  || +0m00.00s
0m00.03s  | Reflection/Rewriter                                                    | 0m00.05s  || -0m00.02s
0m00.03s  | Util/Tactics/SplitInContext                                            | 0m00.04s  || -0m00.01s
0m00.03s  | Util/Tactics/DestructHead                                              | 0m00.03s  || +0m00.00s
0m00.03s  | Util/Tactics/ETransitivity                                             | 0m00.04s  || -0m00.01s
0m00.03s  | Util/Tactics/Test                                                      | 0m00.02s  || +0m00.00s
0m00.03s  | Util/Sigma/Lift                                                        | 0m00.04s  || -0m00.01s
0m00.03s  | Util/IffT                                                              | 0m00.03s  || +0m00.00s
0m00.03s  | Util/Tactics/SetEvars                                                  | 0m00.02s  || +0m00.00s
0m00.03s  | Util/Tactics/PrintContext                                              | 0m00.03s  || +0m00.00s
0m00.03s  | Encoding/EncodingTheorems                                              | 0m00.04s  || -0m00.01s
0m00.03s  | Util/Tactics/Contains                                                  | 0m00.02s  || +0m00.00s
0m00.03s  | Util/GlobalSettings                                                    | 0m00.02s  || +0m00.00s
0m00.03s  | Util/Tactics/SetoidSubst                                               | 0m00.03s  || +0m00.00s
0m00.03s  | Util/Sigma/MapProjections                                              | 0m00.02s  || +0m00.00s
0m00.03s  | Util/Logic                                                             | 0m00.03s  || +0m00.00s
0m00.03s  | Util/Tactics/DebugPrint                                                | 0m00.04s  || -0m00.01s
0m00.02s  | Tactics/VerdiTactics                                                   | 0m00.03s  || -0m00.00s
0m00.02s  | Util/Tactics/Head                                                      | 0m00.03s  || -0m00.00s
0m00.02s  | Util/Tactics/SideConditionsBeforeToAfter                               | 0m00.04s  || -0m00.02s
0m00.02s  | Util/Tactics/Forward                                                   | 0m00.03s  || -0m00.00s
0m00.02s  | Util/LetIn                                                             | 0m00.08s  || -0m00.06s
0m00.02s  | Util/Tactics/EvarExists                                                | 0m00.03s  || -0m00.00s
0m00.02s  | Util/Tactics/ChangeInAll                                               | 0m00.03s  || -0m00.00s
0m00.02s  | Util/Tactics/TransparentAssert                                         | 0m00.03s  || -0m00.00s
0m00.02s  | Util/Tactics/VM                                                        | 0m00.03s  || -0m00.00s
0m00.02s  | Util/Tactics/DestructTrivial                                           | 0m00.02s  || +0m00.00s
0m00.02s  | Util/Tactics/Revert                                                    | 0m00.02s  || +0m00.00s
0m00.02s  | Util/Tactics/DoWithHyp                                                 | 0m00.02s  || +0m00.00s
0m00.02s  | Util/Tactics/MoveLetIn                                                 | 0m00.02s  || +0m00.00s
0m00.02s  | Util/Tactics/SimplifyProjections                                       | 0m00.04s  || -0m00.02s
0m00.02s  | Util/Tactics/SubstEvars                                                | 0m00.03s  || -0m00.00s
0m00.02s  | Util/Notations                                                         | 0m00.04s  || -0m00.02s
0m00.02s  | Util/Tactics/GetGoal                                                   | 0m00.02s  || +0m00.00s
0m00.02s  | Util/Tactics/Not                                                       | 0m00.04s  || -0m00.02s
0m00.02s  | Util/ChangeInAll                                                       | 0m00.03s  || -0m00.00s
0m00.02s  | Util/Tactics/ConvoyDestruct                                            | 0m00.05s  || -0m00.03s
0m00.02s  | Util/Curry                                                             | 0m00.03s  || -0m00.00s
0m00.02s  | Util/Tactics/SimplifyRepeatedIfs                                       | 0m00.03s  || -0m00.00s
0m00.02s  | Util/Isomorphism                                                       | 0m00.04s  || -0m00.02s
0m00.02s  | Util/Tactics/SpecializeBy                                              | 0m00.02s  || +0m00.00s
0m00.02s  | Util/Tactics/OnSubterms                                                | 0m00.02s  || +0m00.00s
0m00.02s  | Util/Tactics/UniquePose                                                | 0m00.04s  || -0m00.02s
0m00.02s  | Util/Unit                                                              | 0m00.05s  || -0m00.03s
0m00.02s  | Spec/Encoding                                                          | 0m00.02s  || +0m00.00s
0m00.02s  | Util/FixCoqMistakes                                                    | 0m00.03s  || -0m00.00s
0m00.02s  | Util/Tactics/ClearDuplicates                                           | 0m00.04s  || -0m00.02s
0m00.02s  | Util/Sigma/Associativity                                               | 0m00.05s  || -0m00.03s
0m00.02s  | Util/Tactics/UnifyAbstractReflexivity                                  | 0m00.02s  || +0m00.00s
0m00.02s  | Util/Tactics/DestructHyps                                              | 0m00.05s  || -0m00.03s
0m00.01s  | Util/Tactics/SubstLet                                                  | 0m00.03s  || -0m00.01s
0m00.00s  | Util/Tactics/ESpecialize                                               | 0m00.02s  || -0m00.02s

9 files changed, 391 insertions, 145 deletions

diff --git a/src/Algebra.v b/src/Algebra.v
index ca86b54e4..342e9feaa 100644
--- a/src/Algebra.v
+++ b/src/Algebra.v
@@ -140,8 +140,15 @@ Section Algebra.
     Global Existing Instance field_div_Proper.
   End AddMul.
 
-  Definition char_ge {T} (eq:T->T->Prop) (zero:T) (inj:BinPos.positive->T) C := forall p, BinPos.Pos.lt p C -> not (eq (inj p) zero).
+  Definition char_ge (zero:T) (inj:BinPos.positive->T) C := forall p, BinPos.Pos.lt p C -> not (eq (inj p) zero).
   Existing Class char_ge.
+  Lemma char_ge_weaken id of_pos C
+        (HC:@char_ge id of_pos C) c (Hc:BinPos.Pos.le c C)
+    : @char_ge id of_pos c.
+  Proof. intros ??; eauto using BinPos.Pos.lt_le_trans. Qed.
+  (* TODO: make a typeclass instance that applies this lemma
+  automatically using [vm_decide] for the inequality if both
+  characteristics are literal constants. *)
 End Algebra.
 
 Section ZeroNeqOne.
diff --git a/src/CompleteEdwardsCurve/EdwardsMontgomery.v b/src/CompleteEdwardsCurve/EdwardsMontgomery.v
index c02e833ac..f5a30ff88 100644
--- a/src/CompleteEdwardsCurve/EdwardsMontgomery.v
+++ b/src/CompleteEdwardsCurve/EdwardsMontgomery.v
@@ -1,15 +1,17 @@
 Require Import Crypto.CompleteEdwardsCurve.CompleteEdwardsCurveTheorems.
 Require Import Crypto.Spec.MontgomeryCurve Crypto.MontgomeryCurveTheorems.
+Require Import Crypto.MontgomeryCurve.
 
 Require Import Crypto.Util.Notations Crypto.Util.Decidable.
 Require Import (*Crypto.Util.Tactics*) Crypto.Util.Sum Crypto.Util.Prod.
 Require Import Crypto.Algebra Crypto.Algebra.Field.
+Import BinNums.
 
 Module E.
   Section EdwardsMontgomery.
     Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}
             {field:@Algebra.field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}
-            {char_ge_3 : @Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul (BinNat.N.succ_pos BinNat.N.two)}
+            {char_ge_28 : @Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul 28}
             {Feq_dec:DecidableRel Feq}.
     Local Infix "=" := Feq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope.
     Local Notation "0" := Fzero.  Local Notation "1" := Fone.
@@ -17,13 +19,18 @@ Module E.
     Local Infix "-" := Fsub. Local Infix "/" := Fdiv.
     Local Notation "x ^ 2" := (x*x).
 
+    Let char_ge_12 : @Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul 12.
+    Proof. eapply char_ge_weaken; eauto. vm_decide. Qed.
+    Let char_ge_3 : @Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul 3.
+    Proof. eapply char_ge_weaken; eauto. vm_decide. Qed.
+
     Context {a d: F}
             {nonzero_a : a <> 0}
             {square_a : exists sqrt_a, sqrt_a^2 = a}
             {nonsquare_d : forall x, x^2 <> d}.
     Local Notation Epoint := (@E.point F Feq Fone Fadd Fmul a d).
     Local Notation Ezero  := (E.zero(nonzero_a:=nonzero_a)(d:=d)).
-    Local Notation Eadd   := (E.add(nonzero_a:=nonzero_a)(square_a:=square_a)(nonsquare_d:=nonsquare_d)).
+    Local Notation Eadd   := (E.add(char_ge_3:=char_ge_3)(nonzero_a:=nonzero_a)(square_a:=square_a)(nonsquare_d:=nonsquare_d)).
     Local Notation Eopp   := (E.opp(nonzero_a:=nonzero_a)(d:=d)).
 
     Let a_neq_d : a <> d.
@@ -86,28 +93,22 @@ Module E.
       assert (f1 <> Fopp 1) by admit (* ad, d are nonsero *); fsatz.
     Admitted.
 
-    Import BinNums.
-    (* TODO: characteristic weakening lemmas *)
-    Context {char_ge_12 : @Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul 12}.
-    Context {char_ge_28 : @Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul 28}.
-
-    Program Definition _EM : _ /\ _ /\ _ :=
+    Program Definition _EM (discr_nonzero:id _) : _ /\ _ /\ _ :=
       @Group.group_from_redundant_representation
         Mpoint M.eq Madd M.zero M.opp
-        (M.group(discr_nonzero:=_))
+        (M.group discr_nonzero)
         Epoint E.eq Eadd Ezero Eopp
         of_Montgomery
         to_Montgomery
         _ _ _ _ _
     .
-    Next Obligation. Proof. Admitted. (* discriminant nonzero *)
-    Next Obligation. Proof. Admitted. (* M->E->M *)
     Next Obligation. Proof. Admitted. (* M->E->M *)
+    Next Obligation. Proof. Admitted. (* equivalences match *)
     Next Obligation. Proof. Admitted. (* add *)
     Next Obligation. Proof. Admitted. (* opp *)
     Next Obligation. Proof. cbv [of_Montgomery to_Montgomery]; t; fsatz. Qed.
 
-    Global Instance homomorphism_of_Montgomery : Monoid.is_homomorphism(phi:=of_Montgomery) := proj1 (proj2 _EM).
-    Global Instance homomorphism_to_Montgomery : Monoid.is_homomorphism(phi:=to_Montgomery) := proj2 (proj2 _EM).
+    Global Instance homomorphism_of_Montgomery discr_nonzero : Monoid.is_homomorphism(phi:=of_Montgomery) := proj1 (proj2 (_EM discr_nonzero)).
+    Global Instance homomorphism_to_Montgomery discr_nonzero : Monoid.is_homomorphism(phi:=to_Montgomery) := proj2 (proj2 (_EM discr_nonzero)).
   End EdwardsMontgomery.
 End E.
diff --git a/src/MontgomeryCurve.v b/src/MontgomeryCurve.v
new file mode 100644
index 000000000..a04701ed5
--- /dev/null
+++ b/src/MontgomeryCurve.v
@@ -0,0 +1,67 @@
+Require Import Crypto.Algebra Crypto.Algebra.Field.
+Require Import Crypto.Util.GlobalSettings.
+Require Import Crypto.Util.Sum Crypto.Util.Prod.
+Require Import Crypto.Util.Tactics.BreakMatch.
+Require Import Crypto.Spec.MontgomeryCurve Crypto.Spec.WeierstrassCurve.
+
+Module M.
+  Section MontgomeryCurve.
+    Import BinNat.
+    Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}
+            {field:@Algebra.field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}
+            {Feq_dec:Decidable.DecidableRel Feq}
+            {char_ge_3:@Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul (BinNat.N.succ_pos (BinNat.N.two))}.
+    Local Infix "=" := Feq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope.
+    Local Infix "+" := Fadd. Local Infix "*" := Fmul.
+    Local Infix "-" := Fsub. Local Infix "/" := Fdiv.
+    Local Notation "- x" := (Fopp x).
+    Local Notation "x ^ 2" := (x*x) (at level 30).
+    Local Notation "x ^ 3" := (x*x^2) (at level 30).
+    Local Notation "0" := Fzero.  Local Notation "1" := Fone.
+    Local Notation "'∞'" := unit : type_scope.
+    Local Notation "'∞'" := (inr tt) : core_scope.
+    Local Notation "( x , y )" := (inl (pair x y)).
+    Local Open Scope core_scope.
+
+    Context {a b: F} {b_nonzero:b <> 0}.
+
+    Program Definition opp (P:@M.point F Feq Fadd Fmul a b) : @M.point F Feq Fadd Fmul a b :=
+      match P return F*F+∞ with
+      | (x, y) => (x, -y)
+      | ∞ => ∞
+      end.
+    Next Obligation. Proof. destruct P; cbv; break_match; trivial; fsatz. Qed.
+
+    Local Notation add := (M.add(b_nonzero:=b_nonzero)).
+    Local Notation point := (@M.point F Feq Fadd Fmul a b).
+
+    Section MontgomeryWeierstrass.
+      Local Notation "2" := (1+1).
+      Local Notation "3" := (1+2).
+      Local Notation "4" := (1+3).
+      Local Notation "16" := (4*4).
+      Local Notation "9" := (3*3).
+      Local Notation "27" := (3*9).
+      Context {char_ge_28:@Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul 28}.
+
+
+      Local Notation WeierstrassA := ((3-a^2)/(3*b^2)).
+      Local Notation WeierstrassB := ((2*a^3-9*a)/(27*b^3)).
+      Local Notation Wpoint := (@W.point F Feq Fadd Fmul WeierstrassA WeierstrassB).
+      Local Notation Wadd := (@W.add F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv field Feq_dec char_ge_3 WeierstrassA WeierstrassB).
+      Program Definition to_Weierstrass (P:@point) : Wpoint :=
+        match M.coordinates P return F*F+∞ with
+        | (x, y) => ((x + a/3)/b, y/b)
+        | _ => ∞
+        end.
+      Next Obligation. Proof. destruct P; cbv; break_match; trivial; fsatz. Qed.
+
+      Program Definition of_Weierstrass (P:Wpoint) : point :=
+        match W.coordinates P return F*F+∞ with
+        | (x,y) => (b*x-a/3, b*y)
+        | _ => ∞
+        end.
+      Next Obligation. Proof. destruct P; cbv; break_match; trivial; fsatz. Qed.
+    End MontgomeryWeierstrass.
+  End MontgomeryCurve.
+End M.
\ No newline at end of file
diff --git a/src/MontgomeryCurveTheorems.v b/src/MontgomeryCurveTheorems.v
index 61eb5f880..7f7ad5bdf 100644
--- a/src/MontgomeryCurveTheorems.v
+++ b/src/MontgomeryCurveTheorems.v
@@ -2,7 +2,8 @@ Require Import Crypto.Algebra Crypto.Algebra.Field.
 Require Import Crypto.Util.GlobalSettings.
 Require Import Crypto.Util.Sum Crypto.Util.Prod.
 Require Import Crypto.Util.Tactics.BreakMatch.
-Require Import Crypto.Spec.MontgomeryCurve Crypto.Spec.WeierstrassCurve.
+Require Import Crypto.Spec.MontgomeryCurve Crypto.MontgomeryCurve.
+Require Import Crypto.Spec.WeierstrassCurve Crypto.WeierstrassCurve.Definitions.
 Require Import Crypto.WeierstrassCurve.WeierstrassCurveTheorems.
 
 Module M.
@@ -11,7 +12,12 @@ Module M.
     Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}
             {field:@Algebra.field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}
             {Feq_dec:Decidable.DecidableRel Feq}
-            {char_ge_3:@Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul (BinNat.N.succ_pos (BinNat.N.two))}.
+            {char_ge_28:@Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul 28}.
+    Let char_ge_12 : @Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul 12.
+    Proof. eapply char_ge_weaken; eauto. vm_decide. Qed.
+    Let char_ge_3 : @Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul 3.
+    Proof. eapply char_ge_weaken; eauto; vm_decide. Qed.
+      
     Local Infix "=" := Feq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope.
     Local Infix "+" := Fadd. Local Infix "*" := Fmul.
     Local Infix "-" := Fsub. Local Infix "/" := Fdiv.
@@ -20,6 +26,7 @@ Module M.
     Local Notation "x ^ 3" := (x*x^2) (at level 30).
     Local Notation "0" := Fzero.  Local Notation "1" := Fone.
     Local Notation "2" := (1+1). Local Notation "3" := (1+2).
+    Local Notation "9" := (3*3). Local Notation "27" := (3*9).
     Local Notation "'∞'" := unit : type_scope.
     Local Notation "'∞'" := (inr tt) : core_scope.
     Local Notation "( x , y )" := (inl (pair x y)).
@@ -27,12 +34,11 @@ Module M.
 
     Context {a b: F} {b_nonzero:b <> 0}.
 
-    Program Definition opp (P:@M.point F Feq Fadd Fmul a b) : @M.point F Feq Fadd Fmul a b :=
-      match P return F*F+∞ with
-      | (x, y) => (x, -y)
-      | ∞ => ∞
-      end.
-    Next Obligation. Proof. destruct P; cbv; break_match; trivial; fsatz. Qed.
+    Local Notation WeierstrassA := ((3-a^2)/(3*b^2)).
+    Local Notation WeierstrassB := ((2*a^3-9*a)/(27*b^3)).
+    Local Notation Wpoint := (@W.point F Feq Fadd Fmul WeierstrassA WeierstrassB).
+    Local Notation Wadd := (@W.add F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv field Feq_dec char_ge_3 WeierstrassA WeierstrassB).
+    Local Notation Wopp := (@W.opp F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv WeierstrassA WeierstrassB field Feq_dec).
 
     Ltac t :=
       repeat
@@ -48,66 +54,29 @@ Module M.
         | _ => progress Prod.inversion_prod
         | _ => progress Tactics.BreakMatch.break_match_hyps
         | _ => progress Tactics.BreakMatch.break_match
-        | _ => progress cbv [M.coordinates M.add M.zero M.eq opp proj1_sig] in *
-        | _ => progress cbv [W.coordinates W.add W.zero W.eq W.inv proj1_sig] in *
+        | _ => progress cbv [M.coordinates M.add M.zero M.eq M.opp proj1_sig
+                             W.coordinates W.add W.zero W.eq W.opp
+                             M.of_Weierstrass M.to_Weierstrass] in *
         | |- _ /\ _ => split | |- _ <-> _ => split
         end.
 
-    Local Notation add := (M.add(b_nonzero:=b_nonzero)).
-    Local Notation point := (@M.point F Feq Fadd Fmul a b).
+    Program Definition _MW (discr_nonzero:id _) : _ /\ _ /\ _ :=
+      @Group.group_from_redundant_representation
+        Wpoint W.eq Wadd W.zero Wopp
+        (abelian_group_group (W.commutative_group(char_ge_12:=char_ge_12)(discriminant_nonzero:=discr_nonzero)))
+        (@M.point F Feq Fadd Fmul a b) M.eq (M.add(char_ge_3:=char_ge_3)(b_nonzero:=b_nonzero)) M.zero (M.opp(b_nonzero:=b_nonzero))
+        (M.of_Weierstrass(b_nonzero:=b_nonzero))
+        (M.to_Weierstrass(b_nonzero:=b_nonzero))
+        _ _ _ _ _
+    .
+    Next Obligation. Proof. t; fsatz. Qed.
+    Next Obligation. Proof. t; fsatz. Qed.
+    Next Obligation. Proof. t; fsatz. Qed.
+    Next Obligation. Proof. t; fsatz. Qed.
+    Next Obligation. Proof. t; fsatz. Qed.
 
-    Section MontgomeryWeierstrass.
-      Local Notation "4" := (1+3).
-      Local Notation "16" := (4*4).
-      Local Notation "9" := (3*3).
-      Local Notation "27" := (3*9).
-      Context {char_ge_28:@Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul 28}.
-
-
-      Local Notation WeierstrassA := ((3-a^2)/(3*b^2)).
-      Local Notation WeierstrassB := ((2*a^3-9*a)/(27*b^3)).
-      Local Notation Wpoint := (@W.point F Feq Fadd Fmul WeierstrassA WeierstrassB).
-      Local Notation Wadd := (@W.add F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv field Feq_dec char_ge_3 WeierstrassA WeierstrassB).
-      Program Definition to_Weierstrass (P:@point) : Wpoint :=
-        match M.coordinates P return F*F+∞ with
-        | (x, y) => ((x + a/3)/b, y/b)
-        | _ => ∞
-        end.
-      Next Obligation. Proof. t; fsatz. Qed.
-
-      Program Definition of_Weierstrass (P:Wpoint) : point :=
-        match W.coordinates P return F*F+∞ with
-        | (x,y) => (b*x-a/3, b*y)
-        | _ => ∞
-        end.
-      Next Obligation. Proof. t. fsatz. Qed.
-
-      (*TODO: rename inv to opp, make it not require [discr_nonzero] *)
-      Context {discr_nonzero : (2 + 1 + 1) * WeierstrassA * WeierstrassA * WeierstrassA +
-                               ((2 + 1 + 1) ^ 2 + (2 + 1 + 1) + (2 + 1 + 1) + 1 + 1 + 1) *
-                               WeierstrassB * WeierstrassB <> 0}.
-      (* TODO: weakening lemma for characteristic *)
-      Context {char_ge_12:@Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul 12}.
-      Local Notation Wopp := (@W.inv F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv WeierstrassA WeierstrassB field Feq_dec discr_nonzero).
-
-      Program Definition _MW : _ /\ _ /\ _ :=
-        @Group.group_from_redundant_representation
-          Wpoint W.eq Wadd W.zero Wopp
-          (abelian_group_group (W.commutative_group(discriminant_nonzero:=discr_nonzero)))
-          point M.eq (M.add(b_nonzero:=b_nonzero)) M.zero opp
-          of_Weierstrass
-          to_Weierstrass
-          _ _ _ _ _
-      .
-      Next Obligation. Proof. cbv [of_Weierstrass to_Weierstrass]; t; clear discr_nonzero; fsatz. Qed.
-      Next Obligation. Proof. cbv [of_Weierstrass to_Weierstrass]; t; clear discr_nonzero; fsatz. Qed.
-      Next Obligation. Proof. cbv [of_Weierstrass to_Weierstrass]; t; clear discr_nonzero; fsatz. Qed.
-      Next Obligation. Proof. cbv [of_Weierstrass to_Weierstrass]; t; clear discr_nonzero; fsatz. Qed.
-      Next Obligation. Proof. cbv [of_Weierstrass to_Weierstrass]; t; clear discr_nonzero; fsatz. Qed.
-
-      Global Instance group : Algebra.group := proj1 _MW.
-      Global Instance homomorphism_of_Weierstrass : Monoid.is_homomorphism(phi:=of_Weierstrass) := proj1 (proj2 _MW).
-      Global Instance homomorphism_to_Weierstrass : Monoid.is_homomorphism(phi:=to_Weierstrass) := proj2 (proj2 _MW).
-    End MontgomeryWeierstrass.
+    Global Instance group discr_nonzero : Algebra.group := proj1 (_MW discr_nonzero).
+    Global Instance homomorphism_of_Weierstrass discr_nonzero : Monoid.is_homomorphism(phi:=M.of_Weierstrass) := proj1 (proj2 (_MW discr_nonzero)).
+    Global Instance homomorphism_to_Weierstrass discr_nonzero : Monoid.is_homomorphism(phi:=M.to_Weierstrass) := proj2 (proj2 (_MW discr_nonzero)).
   End MontgomeryCurve.
 End M.
diff --git a/src/MontgomeryX.v b/src/MontgomeryX.v
index a9cbd8836..6cb5b2387 100644
--- a/src/MontgomeryX.v
+++ b/src/MontgomeryX.v
@@ -1,7 +1,7 @@
 Require Import Crypto.Algebra Crypto.Algebra.Field.
 Require Import Crypto.Util.GlobalSettings Crypto.Util.Notations.
 Require Import Crypto.Util.Sum Crypto.Util.Prod Crypto.Util.LetIn.
-Require Import Crypto.Spec.MontgomeryCurve Crypto.MontgomeryCurveTheorems.
+Require Import Crypto.Spec.MontgomeryCurve Crypto.MontgomeryCurve.
 
 Module M.
   Section MontgomeryCurve.
@@ -9,7 +9,6 @@ Module M.
     Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}
             {field:@Algebra.field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}
             {Feq_dec:Decidable.DecidableRel Feq}
-            {char_ge_3:@Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul (BinNat.N.succ_pos (BinNat.N.two))}
             {char_ge_5:@Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul 5}.
     Local Infix "=" := Feq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope.
     Local Infix "+" := Fadd. Local Infix "*" := Fmul.
@@ -30,6 +29,9 @@ Module M.
       | ∞ => pair 1 0
       end.
 
+    Let char_ge_3:@Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul (BinNat.N.succ_pos (BinNat.N.two)).
+    Proof. eapply char_ge_weaken; eauto; vm_decide. Qed.
+
     (* From Curve25519 paper by djb, appendix B. Credited to Montgomery *)
     Context {a24:F} {a24_correct:(1+1+1+1)*a24 = a-(1+1)}.
     Definition xzladderstep (x1:F) (Q Q':F*F) : ((F*F)*(F*F)) :=
@@ -50,33 +52,5 @@ Module M.
         dlet z3 := x1*(DA-CB)^2 in
         (pair (pair x2 z2) (pair x3 z3))
       end.
-
-    Ltac t :=
-      repeat
-        match goal with
-        | _ => solve [ contradiction | trivial ]
-        | _ => progress intros
-        | _ => progress subst
-        | _ => progress Tactics.DestructHead.destruct_head' @M.point
-        | _ => progress Tactics.DestructHead.destruct_head' @prod
-        | _ => progress Tactics.DestructHead.destruct_head' @sum
-        | _ => progress Tactics.DestructHead.destruct_head' @and
-        | _ => progress Sum.inversion_sum
-        | _ => progress Prod.inversion_prod
-        | _ => progress Tactics.BreakMatch.break_match_hyps
-        | _ => progress Tactics.BreakMatch.break_match
-        | _ => progress cbv [fst snd M.coordinates M.add M.zero M.eq M.opp proj1_sig xzladderstep to_xz Let_In] in *
-        | |- _ /\ _ => split
-        end.
-
-    Lemma xzladderstep_correct
-          (Q Q':point) x z x' z' x1 x2 z2 x3 z3
-          (Hl:Logic.eq (pair(pair x2 z2)(pair x3 z3)) (xzladderstep x1 (pair x z) (pair x' z')))
-          (H:match M.coordinates Q with∞=>z=0/\x<>0|(xQ,y)=>xQ=x/z/\z<>0  (* TODO *) /\ y <> 0 (* TODO: prove this from non-squareness of a^2 - 4 *) end)
-          (H':match M.coordinates Q' with∞=>z'=0/\x'<>0|(xQ',_)=>xQ'=x'/z'/\z'<>0 end)
-          (H1:match M.coordinates (add Q (opp Q')) with∞=>False|(x,y)=>x=x1/\x<>0 end):
-      match M.coordinates (add Q Q) with∞=>z2=0/\x2<>0|(xQQ,_)=>xQQ=x2/z2/\z2<>0 end /\
-      match M.coordinates (add Q Q') with∞=>z3=0/\x3<>0|(xQQ',_)=>xQQ'=x3/z3/\z3<>0 end.
-    Proof using a24_correct char_ge_5. t; abstract fsatz. Qed.
   End MontgomeryCurve.
 End M.
diff --git a/src/MontgomeryXProofs.v b/src/MontgomeryXProofs.v
new file mode 100644
index 000000000..f3f0346c9
--- /dev/null
+++ b/src/MontgomeryXProofs.v
@@ -0,0 +1,57 @@
+Require Import Crypto.Algebra Crypto.Algebra.Field.
+Require Import Crypto.Util.Sum Crypto.Util.Prod Crypto.Util.LetIn.
+Require Import Crypto.Spec.MontgomeryCurve Crypto.MontgomeryCurve.
+Require Import Crypto.MontgomeryX BinPos.
+
+Module M.
+  Section MontgomeryCurve.
+    Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}
+            {field:@Algebra.field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}
+            {Feq_dec:Decidable.DecidableRel Feq}
+            {char_ge_5:@Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul 5}.
+    Local Infix "=" := Feq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope.
+    Local Infix "+" := Fadd. Local Infix "*" := Fmul.
+    Local Infix "-" := Fsub. Local Infix "/" := Fdiv.
+    Local Notation "0" := Fzero.  Local Notation "1" := Fone.
+    Local Notation "'∞'" := (inr tt) : core_scope.
+    Local Notation "( x , y )" := (inl (pair x y)).
+
+    Let char_ge_3:@Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul (BinNat.N.succ_pos (BinNat.N.two)).
+    Proof. eapply char_ge_weaken; eauto; vm_decide. Qed.
+
+    Context {a b: F} {b_nonzero:b <> 0}.
+    Context {a24:F} {a24_correct:(1+1+1+1)*a24 = a-(1+1)}.
+    Local Notation add := (M.add(a:=a)(b_nonzero:=b_nonzero)(char_ge_3:=char_ge_3)).
+    Local Notation opp := (M.opp(a:=a)(b_nonzero:=b_nonzero)).
+    Local Notation point := (@M.point F Feq Fadd Fmul a b).
+    Local Notation xzladderstep := (M.xzladderstep(a24:=a24)(Fadd:=Fadd)(Fsub:=Fsub)(Fmul:=Fmul)).
+
+    Ltac t :=
+      repeat
+        match goal with
+        | _ => solve [ contradiction | trivial ]
+        | _ => progress intros
+        | _ => progress subst
+        | _ => progress Tactics.DestructHead.destruct_head' @M.point
+        | _ => progress Tactics.DestructHead.destruct_head' @prod
+        | _ => progress Tactics.DestructHead.destruct_head' @sum
+        | _ => progress Tactics.DestructHead.destruct_head' @and
+        | _ => progress Sum.inversion_sum
+        | _ => progress Prod.inversion_prod
+        | _ => progress Tactics.BreakMatch.break_match_hyps
+        | _ => progress Tactics.BreakMatch.break_match
+        | _ => progress cbv [fst snd M.coordinates M.add M.zero M.eq M.opp proj1_sig M.xzladderstep M.to_xz Let_In] in *
+        | |- _ /\ _ => split
+        end.
+
+    Lemma xzladderstep_correct
+          (Q Q':point) x z x' z' x1 x2 z2 x3 z3
+          (Hl:Logic.eq (pair(pair x2 z2)(pair x3 z3)) (xzladderstep x1 (pair x z) (pair x' z')))
+          (H:match M.coordinates Q with∞=>z=0/\x<>0|(xQ,y)=>xQ=x/z/\z<>0  (* TODO *) /\ y <> 0 (* TODO: prove this from non-squareness of a^2 - 4 *) end)
+          (H':match M.coordinates Q' with∞=>z'=0/\x'<>0|(xQ',_)=>xQ'=x'/z'/\z'<>0 end)
+          (H1:match M.coordinates (add Q (opp Q')) with∞=>False|(x,y)=>x=x1/\x<>0 end):
+      match M.coordinates (add Q Q) with∞=>z2=0/\x2<>0|(xQQ,_)=>xQQ=x2/z2/\z2<>0 end /\
+      match M.coordinates (add Q Q') with∞=>z3=0/\x3<>0|(xQQ',_)=>xQQ'=x3/z3/\z3<>0 end.
+    Proof using a24_correct char_ge_5. t; abstract fsatz. Qed.
+  End MontgomeryCurve.
+End M.
diff --git a/src/Util/Decidable.v b/src/Util/Decidable.v
index e7e8ce471..2703ef108 100644
--- a/src/Util/Decidable.v
+++ b/src/Util/Decidable.v
@@ -11,7 +11,6 @@ Local Open Scope type_scope.
 
 Class Decidable (P : Prop) := dec : {P} + {~P}.
 Arguments dec _%type_scope {_}.
-
 Notation DecidableRel R := (forall x y, Decidable (R x y)).
 
 Global Instance hprop_eq_dec {A} `{DecidableRel (@eq A)} : IsHPropRel (@eq A) | 10.
@@ -85,7 +84,6 @@ Lemma dec_not {A} `{Decidable A} : Decidable (~A).
 Proof. solve_decidable_transparent. Defined.
 (** Disallow infinite loops of dec_not *)
 Hint Extern 0 (Decidable (~?A)) => apply (@dec_not A) : typeclass_instances.
-
 Global Instance dec_eq_unit : DecidableRel (@eq unit) | 10. exact _. Defined.
 Global Instance dec_eq_bool : DecidableRel (@eq bool) | 10. exact _. Defined.
 Global Instance dec_eq_Empty_set : DecidableRel (@eq Empty_set) | 10. exact _. Defined.
@@ -110,8 +108,6 @@ Global Instance dec_le_Z : DecidableRel BinInt.Z.le := ZArith_dec.Z_le_dec.
 Global Instance dec_gt_Z : DecidableRel BinInt.Z.gt := ZArith_dec.Z_gt_dec.
 Global Instance dec_ge_Z : DecidableRel BinInt.Z.ge := ZArith_dec.Z_ge_dec.
 
-Global Instance dec_eq_positive : DecidableRel (@eq BinNums.positive) | 10 := BinPos.Pos.eq_dec.
-
 Global Instance dec_match_pair {A B} {P : A -> B -> Prop} {x : A * B}
        {HD : Decidable (P (fst x) (snd x))}
   : Decidable (let '(a, b) := x in P a b) | 1.
@@ -139,6 +135,16 @@ Proof. solve_decidable_transparent. Defined.
 Lemma Decidable_iff_to_flip_impl A B (H : A <-> B) : Decidable B -> Decidable A.
 Proof. solve_decidable_transparent. Defined.
 
+Global Instance dec_eq_positive : DecidableRel (@eq BinNums.positive) | 10 := BinPos.Pos.eq_dec.
+Global Instance dec_lt_positive : DecidableRel BinPos.Pos.lt.
+Proof. eauto using Decidable_iff_to_impl, Pos.ltb_lt with typeclass_instances. Defined.
+Global Instance dec_le_positive : DecidableRel BinPos.Pos.le.
+Proof. eauto using Decidable_iff_to_impl, Pos.leb_le with typeclass_instances. Defined.
+Global Instance dec_gt_positive : DecidableRel BinPos.Pos.gt.
+Proof. eauto using Decidable_iff_to_flip_impl, Pos.gt_lt_iff with typeclass_instances. Defined.
+Global Instance dec_ge_positive : DecidableRel BinPos.Pos.ge.
+Proof. eauto using Decidable_iff_to_flip_impl, Pos.ge_le_iff with typeclass_instances. Defined.
+
 Lemma dec_of_semidec {P : Prop} (H : option P) (H_complete : H = None -> ~P) : Decidable P.
 Proof. destruct H; [ left; assumption | right; apply H_complete, eq_refl ]. Defined.
 
@@ -169,4 +175,4 @@ Lemma cast_if_eq_refl {T H P} t v : @cast_if_eq T H P t t v = Some v.
 Proof.
   compute; clear; destruct (H t t) as [ [] |e];
     [ reflexivity | destruct (e eq_refl) ].
-Qed.
+Qed.
\ No newline at end of file
diff --git a/src/WeierstrassCurve/Definitions.v b/src/WeierstrassCurve/Definitions.v
new file mode 100644
index 000000000..fb400d8c8
--- /dev/null
+++ b/src/WeierstrassCurve/Definitions.v
@@ -0,0 +1,18 @@
+Require Import Crypto.Spec.WeierstrassCurve.
+Require Import Crypto.Algebra Crypto.Algebra.Field.
+Require Import Crypto.Util.Decidable Crypto.Util.Tactics.DestructHead Crypto.Util.Tactics.BreakMatch.
+
+Module W.
+  Section W.
+    Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} {a b:F}
+            {field:@Algebra.field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}
+            {Feq_dec:DecidableRel Feq}.
+
+    Program Definition opp (P:@W.point F Feq Fadd Fmul a b) : @W.point F Feq Fadd Fmul a b
+      := match W.coordinates P return F*F+_ with
+         | inl (x1, y1) => inl (x1, Fopp y1)
+         | _ => P
+         end.
+    Next Obligation. destruct P as [[[??]|[]]?]; cbv; trivial; fsatz. Qed.
+  End W.
+End W.
\ No newline at end of file
diff --git a/src/WeierstrassCurve/WeierstrassCurveTheorems.v b/src/WeierstrassCurve/WeierstrassCurveTheorems.v
index 38dda01d6..7547eb147 100644
--- a/src/WeierstrassCurve/WeierstrassCurveTheorems.v
+++ b/src/WeierstrassCurve/WeierstrassCurveTheorems.v
@@ -1,6 +1,6 @@
 Require Import Coq.Numbers.BinNums.
 Require Import Coq.Classes.Morphisms.
-Require Import Crypto.Spec.WeierstrassCurve.
+Require Import Crypto.Spec.WeierstrassCurve Crypto.WeierstrassCurve.Definitions.
 Require Import Crypto.Algebra Crypto.Algebra.Field.
 Require Import Crypto.Util.Decidable Crypto.Util.Tactics.DestructHead Crypto.Util.Tactics.BreakMatch.
 Require Import Coq.PArith.BinPos.
@@ -9,41 +9,188 @@ Module W.
   Section W.
     Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} {a b:F}
             {field:@Algebra.field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}
-            {char_ge_3:@Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul (BinNat.N.succ_pos (BinNat.N.two))}
-            {char_ge_12:@Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul 12%positive} (* FIXME: shouldn't need we need 4, not 12? *)
-            {Feq_dec:DecidableRel Feq}.
+            {Feq_dec:DecidableRel Feq}
+            {char_ge_12:@Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul 12%positive}. (* FIXME: shouldn't need we need 4, not 12? *)
+    Let char_ge_3 : @Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul 3.
+    Proof. eapply char_ge_weaken; eauto; vm_decide. Qed.
     Local Infix "=" := Feq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope.
     Local Notation "0" := Fzero.  Local Notation "1" := Fone.
     Local Infix "+" := Fadd. Local Infix "-" := Fsub. Local Infix "*" := Fmul.
     Local Notation "4" := (1+1+1+1). Local Notation "27" := (4*4 + 4+4 +1+1+1).
-    Context {discriminant_nonzero:4*a*a*a + 27*b*b <> 0}.
 
-    Program Definition inv (P:@W.point F Feq Fadd Fmul a b) : @W.point F Feq Fadd Fmul a b
-      := match W.coordinates P return F*F+_ with
-         | inl (x1, y1) => inl (x1, Fopp y1)
-         | _ => P
-         end.
-    Next Obligation. destruct P as [[[??]|[]]?]; cbv; trivial; fsatz. Qed.
+    Global Instance commutative_group {discriminant_nonzero:id(4*a*a*a + 27*b*b <> 0)} : abelian_group(eq:=W.eq(a:=a)(b:=b))(op:=W.add(char_ge_3:=char_ge_3))(id:=W.zero)(inv:=W.opp).
+    Proof using Type.
+      Time
+        repeat match goal with
+               | _ => solve [ contradiction | trivial | exact _ ]
+               | _ => intro
+               | |- Equivalence _ => split
+               | |- abelian_group => split | |- group => split | |- monoid => split
+               | |- is_associative => split | |- is_commutative => split
+               | |- is_left_inverse => split | |- is_right_inverse => split
+               | |- is_left_identity => split | |- is_right_identity => split
+               | _ => progress destruct_head' @W.point
+               | _ => progress destruct_head' sum
+               | _ => progress destruct_head' prod
+               | _ => progress destruct_head' unit
+               | _ => progress destruct_head' and
+               | _ => progress cbv [W.opp W.eq W.zero W.add W.coordinates proj1_sig]in*
+               | _ => progress break_match
+               end.
+      (* Finished transaction in 2.098 secs (2.099u,0.s) (successful) *)
+      all:  try split.
+      (* Finished transaction in 0.052 secs (0.053u,0.s) (successful) *)
 
-    Global Instance commutative_group : abelian_group(eq:=W.eq)(op:=W.add)(id:=W.zero)(inv:=inv).
-    Proof using Feq_dec discriminant_nonzero field char_ge_12.
-      repeat match goal with
-             | _ => solve [ contradiction | trivial | exact _ ]
-             | _ => intro
-             | |- Equivalence _ => split
-             | |- abelian_group => split | |- group => split | |- monoid => split
-             | |- is_associative => split | |- is_commutative => split
-             | |- is_left_inverse => split | |- is_right_inverse => split
-             | |- is_left_identity => split | |- is_right_identity => split
-             | _ => progress destruct_head' @W.point
-             | _ => progress destruct_head' sum
-             | _ => progress destruct_head' prod
-             | _ => progress destruct_head' unit
-             | _ => progress destruct_head' and
-             | _ => progress cbv [inv W.eq W.zero W.add W.coordinates proj1_sig]in*
-             | _ => progress break_match
-             end.
-      all: try abstract(fsatz_prepare_hyps; repeat split; fsatz_solve).
-    Qed.
+      (* The [discriminant_nonzero] hypothesis makes [fsatz] slow but
+      is necessary in some cases. Thus, we wrap it in [id] by detault
+      to hide it from [nsatz] but unfold it when normal [fsatz] fails. *)
+      (* Variable re-ordering is a micro-optimization *)
+      (* TODO: why does par not work here? *)
+      Ltac s := abstract (
+                    match goal with [H:id _ |- _] => move H at bottom end;
+                    move b at bottom;
+                    move a at bottom;
+                    repeat match goal with [H: ?x = Fopp ?y |- _] => is_var x; is_var y; revert H end; intros;
+                    repeat match goal with [H: ?x = ?y |- _] => is_var x; is_var y; revert H end; intros;
+                    repeat split;
+                    solve
+                      [ fsatz
+                      | cbv [id] in *; fsatz]
+                  ).
+      Time s. (* Finished transaction in 0.099 secs (0.096u,0.003s) (successful) *)
+      Time s. (* Finished transaction in 0.094 secs (0.093u,0.s) (successful) *)
+      Time s. (* Finished transaction in 0.48 secs (0.48u,0.s) (successful) *)
+      Time s. (* Finished transaction in 2.229 secs (2.226u,0.003s) (successful) *)
+      Time s. (* Finished transaction in 3.164 secs (3.153u,0.01s) (successful) *)
+      Time s. (* Finished transaction in 2.218 secs (2.199u,0.019s) (successful) *)
+      Time s. (* Finished transaction in 3.499 secs (3.486u,0.01s) (successful) *)
+      Time s. (* Finished transaction in 1.164 secs (1.16u,0.003s) (successful) *)
+      Time s. (* Finished transaction in 1.971 secs (1.953u,0.016s) (successful) *)
+      Time s. (* Finished transaction in 2.344 secs (2.343u,0.003s) (successful) *)
+      Time s. (* Finished transaction in 1.287 secs (1.286u,0.s) (successful) *)
+      Time s. (* Finished transaction in 1.781 secs (1.783u,0.s) (successful) *)
+      Time s. (* Finished transaction in 0.497 secs (0.496u,0.s) (successful) *)
+      Time s. (* Finished transaction in 1.859 secs (1.856u,0.003s) (successful) *)
+      Time s. (* Finished transaction in 1.499 secs (1.499u,0.s) (successful) *)
+      Time s. (* Finished transaction in 1.6 secs (1.6u,0.s) (successful) *)
+      Time s. (* Finished transaction in 1.446 secs (1.443u,0.s) (successful) *)
+      Time s. (* Finished transaction in 1.56 secs (1.563u,0.s) (successful) *)
+      Time s. (* Finished transaction in 1.62 secs (1.616u,0.003s) (successful) *)
+      Time s. (* Finished transaction in 1.973 secs (1.966u,0.006s) (successful) *)
+      Time s. (* Finished transaction in 7.66 secs (7.663u,0.s) (successful) *)
+      Time s. (* Finished transaction in 7.645 secs (7.643u,0.003s) (successful) *)
+      Time s. (* Finished transaction in 5.956 secs (5.949u,0.006s) (successful) *)
+      Time s. (* Finished transaction in 7.835 secs (7.803u,0.s) (successful) *)
+      Time s. (* Finished transaction in 1.893 secs (1.893u,0.s) (successful) *)
+      Time s. (* Finished transaction in 10.23 secs (10.229u,0.003s) (successful) *)
+      Time s. (* Finished transaction in 11.059 secs (11.036u,0.02s) (successful) *)
+      Time s. (* Finished transaction in 8.965 secs (8.963u,0.s) (successful) *)
+      Time s. (* Finished transaction in 9.539 secs (9.539u,0.003s) (successful) *)
+      Time s. (* Finished transaction in 2.019 secs (2.013u,0.003s) (successful) *)
+      Time s. (* Finished transaction in 2.907 secs (2.9u,0.01s) (successful) *)
+      Time s. (* Finished transaction in 1.622 secs (1.613u,0.01s) (successful) *)
+      Time s. (* Finished transaction in 13.205 secs (13.203u,0.003s) (successful) *)
+      Time s. (* Finished transaction in 14.689 secs (14.686u,0.s) (successful) *)
+      Time s. (* Finished transaction in 10.672 secs (10.673u,0.s) (successful) *)
+      Time s. (* Finished transaction in 13.509 secs (13.509u,0.s) (successful) *)
+      Time s. (* Finished transaction in 1.389 secs (1.386u,0.003s) (successful) *)
+      Time s. (* Finished transaction in 10.331 secs (10.329u,0.003s) (successful) *)
+      Time s. (* Finished transaction in 12.182 secs (12.176u,0.006s) (successful) *)
+      Time s. (* Finished transaction in 9.826 secs (9.829u,0.s) (successful) *)
+      Time s. (* Finished transaction in 13.709 secs (13.703u,0.003s) (successful) *)
+      Time s. (* Finished transaction in 1.059 secs (1.06u,0.s) (successful) *)
+      Time s. (* Finished transaction in 1.894 secs (1.896u,0.s) (successful) *)
+      Time s. (* Finished transaction in 1.358 secs (1.356u,0.003s) (successful) *)
+      Time s. (* Finished transaction in 1.537 secs (1.536u,0.s) (successful) *)
+      Time s. (* Finished transaction in 1.342 secs (1.343u,0.s) (successful) *)
+      Time s. (* Finished transaction in 1.095 secs (1.096u,0.s) (successful) *)
+      Time s. (* Finished transaction in 1.157 secs (1.153u,0.003s) (successful) *)
+      Time s. (* Finished transaction in 1.603 secs (1.603u,0.s) (successful) *)
+      Time s. (* Finished transaction in 6.196 secs (6.196u,0.s) (successful) *)
+      Time s. (* Finished transaction in 6.949 secs (6.949u,0.s) (successful) *)
+      Time s. (* Finished transaction in 4.685 secs (4.68u,0.006s) (successful) *)
+      Time s. (* Finished transaction in 6.483 secs (6.483u,0.s) (successful) *)
+      Time s. (* Finished transaction in 1.451 secs (1.453u,0.s) (successful) *)
+      Time s. (* Finished transaction in 13.648 secs (13.646u,0.s) (successful) *)
+      Time s. (* Finished transaction in 18.053 secs (18.056u,0.s) (successful) *)
+      Time s. (* Finished transaction in 7.186 secs (7.186u,0.s) (successful) *)
+      Time s. (* Finished transaction in 8.817 secs (8.819u,0.s) (successful) *)
+      Time s. (* Finished transaction in 1.251 secs (1.25u,0.s) (successful) *)
+      Time s. (* Finished transaction in 1.569 secs (1.569u,0.s) (successful) *)
+      Time s. (* Finished transaction in 1.356 secs (1.356u,0.s) (successful) *)
+      Time s. (* Finished transaction in 11.45 secs (11.446u,0.003s) (successful) *)
+      Time s. (* Finished transaction in 17.968 secs (17.969u,0.003s) (successful) *)
+      Time s. (* Finished transaction in 12.418 secs (12.366u,0.046s) (successful) *)
+      Time s. (* Finished transaction in 15.323 secs (15.316u,0.01s) (successful) *)
+      Time s. (* Finished transaction in 1.589 secs (1.586u,0.003s) (successful) *)
+      Time s. (* Finished transaction in 10.22 secs (10.223u,0.s) (successful) *)
+      Time s. (* Finished transaction in 11.887 secs (11.889u,0.s) (successful) *)
+      Time s. (* Finished transaction in 7.284 secs (7.283u,0.003s) (successful) *)
+      Time s. (* Finished transaction in 8.75 secs (8.753u,0.s) (successful) *)
+      Time s. (* Finished transaction in 0.291 secs (0.29u,0.s) (successful) *)
+      Time s. (* Finished transaction in 0.348 secs (0.346u,0.s) (successful) *)
+      Time s. (* Finished transaction in 0.222 secs (0.223u,0.s) (successful) *)
+      Time s. (* Finished transaction in 0.266 secs (0.266u,0.s) (successful) *)
+      Time s. (* Finished transaction in 0.296 secs (0.296u,0.s) (successful) *)
+      Time s. (* Finished transaction in 0.737 secs (0.736u,0.s) (successful) *)
+      Time s. (* Finished transaction in 0.227 secs (0.226u,0.s) (successful) *)
+      Time s. (* Finished transaction in 0.269 secs (0.269u,0.s) (successful) *)
+      Time s. (* Finished transaction in 0.054 secs (0.056u,0.s) (successful) *)
+      Time s. (* Finished transaction in 0.057 secs (0.056u,0.s) (successful) *)
+      Time s. (* Finished transaction in 0.308 secs (0.309u,0.s) (successful) *)
+      Time s. (* Finished transaction in 0.362 secs (0.363u,0.s) (successful) *)
+      Time s. (* Finished transaction in 0.226 secs (0.226u,0.s) (successful) *)
+      Time s. (* Finished transaction in 0.279 secs (0.279u,0.s) (successful) *)
+      Time s. (* Finished transaction in 0.055 secs (0.053u,0.s) (successful) *)
+      Time s. (* Finished transaction in 0.052 secs (0.053u,0.s) (successful) *)
+      Time s. (* Finished transaction in 0.057 secs (0.06u,0.s) (successful) *)
+      Time s. (* Finished transaction in 0.053 secs (0.053u,0.s) (successful) *)
+      Time s. (* Finished transaction in 0.052 secs (0.049u,0.s) (successful) *)
+      Time s. (* Finished transaction in 0.053 secs (0.056u,0.s) (successful) *)
+      Time s. (* Finished transaction in 0.055 secs (0.053u,0.s) (successful) *)
+      Time s. (* Finished transaction in 0.053 secs (0.053u,0.s) (successful) *)
+      Time s. (* Finished transaction in 0.2 secs (0.203u,0.s) (successful) *)
+      Time s. (* Finished transaction in 0.21 secs (0.21u,0.s) (successful) *)
+      Time s. (* Finished transaction in 0.208 secs (0.206u,0.s) (successful) *)
+      Time s. (* Finished transaction in 1.162 secs (1.163u,0.s) (successful) *)
+      Time s. (* Finished transaction in 1.256 secs (1.256u,0.s) (successful) *)
+      Time s. (* Finished transaction in 0.994 secs (0.996u,0.s) (successful) *)
+      Time s. (* Finished transaction in 1.017 secs (1.016u,0.s) (successful) *)
+      Time s. (* Finished transaction in 0.186 secs (0.186u,0.s) (successful) *)
+      Time s. (* Finished transaction in 1.044 secs (1.043u,0.s) (successful) *)
+      Time s. (* Finished transaction in 1.123 secs (1.123u,0.s) (successful) *)
+      Time s. (* Finished transaction in 0.892 secs (0.889u,0.s) (successful) *)
+      Time s. (* Finished transaction in 0.961 secs (0.963u,0.s) (successful) *)
+      Time s. (* Finished transaction in 0.051 secs (0.05u,0.s) (successful) *)
+      Time s. (* Finished transaction in 0.052 secs (0.053u,0.s) (successful) *)
+      Time s. (* Finished transaction in 0.085 secs (0.086u,0.s) (successful) *)
+      Time s. (* Finished transaction in 0.081 secs (0.08u,0.s) (successful) *)
+      Time s. (* Finished transaction in 0.12 secs (0.119u,0.s) (successful) *)
+      Time s. (* Finished transaction in 0.116 secs (0.12u,0.s) (successful) *)
+      Time s. (* Finished transaction in 0.074 secs (0.073u,0.s) (successful) *)
+      Time s. (* Finished transaction in 0.067 secs (0.066u,0.s) (successful) *)
+      Time s. (* Finished transaction in 0.07 secs (0.073u,0.s) (successful) *)
+      Time s. (* Finished transaction in 0.063 secs (0.063u,0.s) (successful) *)
+      Time s. (* Finished transaction in 0.083 secs (0.083u,0.s) (successful) *)
+      Time s. (* Finished transaction in 0.084 secs (0.083u,0.s) (successful) *)
+      Time s. (* Finished transaction in 0.106 secs (0.106u,0.s) (successful) *)
+      Time s. (* Finished transaction in 0.097 secs (0.096u,0.s) (successful) *)
+      Time s. (* Finished transaction in 0.108 secs (0.106u,0.s) (successful) *)
+      Time s. (* Finished transaction in 0.658 secs (0.66u,0.s) (successful) *)
+      Time s. (* Finished transaction in 0.775 secs (0.773u,0.s) (successful) *)
+      Time s. (* Finished transaction in 0.527 secs (0.526u,0.s) (successful) *)
+      Time s. (* Finished transaction in 0.625 secs (0.623u,0.003s) (successful) *)
+      Time s. (* Finished transaction in 0.106 secs (0.106u,0.s) (successful) *)
+      Time s. (* Finished transaction in 0.586 secs (0.586u,0.s) (successful) *)
+      Time s. (* Finished transaction in 0.687 secs (0.686u,0.s) (successful) *)
+      Time s. (* Finished transaction in 0.189 secs (0.189u,0.s) (successful) *)
+      Time s. (* Finished transaction in 0.21 secs (0.209u,0.s) (successful) *)
+      Time s. (* Finished transaction in 0.066 secs (0.066u,0.s) (successful) *)
+      Time s. (* Finished transaction in 0.078 secs (0.08u,0.s) (successful) *)
+      Time s. (* Finished transaction in 0.083 secs (0.083u,0.s) (successful) *)
+      Time s. (* Finished transaction in 0.068 secs (0.066u,0.s) (successful) *)
+      (* Total: 414.396 seconds, roughly 7 minutes*)
+
+    Time Qed.
   End W.
 End W.