clean elliptic curve proofs, use par: in WeierstrassAffineProofs

This required working fsatz around
<https://coq.inria.fr/bugs/show_bug.cgi?id=5452>;
par: abstract (abstract tac) raises anomalies

Curves/Weierstrass/AffineProofs is still affected by something like
<https://coq.inria.fr/bugs/show_bug.cgi?id=4831>;
par: Goals randomly not solved

The timing script ran out of memory the first time, so I winged the last
couple of files that were left.

src/Curves/Weierstrass/AffineProofs (real: 516.30, user: 757.86, sys: 2.52, mem: 2808940 ko), was: 14m49s
src/Curves/Montgomery/AffineProofs (real: 51.38, user: 50.82, sys: 0.48, mem: 1509924 ko),    was:    55s
src/Curves/Edwards/Montgomery (real: 4.55, user: 4.43, sys: 0.09, mem: 542008 ko),            was:     5s
src/Curves/Montgomery/XZProofs (real: 36.27, user: 35.87, sys: 0.32, mem: 1391216 ko),        was:    39s
src/Specific/IntegrationTestLadderstep (real: 158.95, user: 158.42, sys: 0.50, mem: 1827860 ko)was: 3m10s

0m43.48s  | Specific/IntegrationTestLadderstep                           | 3m10.35s  || -2m00.87s
3m08.45s  | Curves/Weierstrass/Projective                                | 2m39.76s  || +0m00.68s
2m13.43s  | Spec/Test/X25519                                             | 2m11.48s  || +0m00.95s
1m23.64s  | Specific/IntegrationTestLadderstep130                        | 1m20.78s  || +0m00.85s
1m05.88s  | Compilers/Z/ArithmeticSimplifierWf                           | 1m01.03s  || +0m00.84s
1m01.96s  | Spec/Ed25519                                                 | 0m55.02s  || +0m00.93s
0m33.80s  | Curves/Edwards/XYZT                                          | 0m25.10s  || +0m00.69s
0m30.97s  | Curves/Edwards/AffineProofs                                  | 0m29.76s  || +0m00.20s
0m24.12s  | Compilers/Named/MapCastWf                                    | 0m24.19s  || -0m00.07s
0m23.94s  | Primitives/EdDSARepChange                                    | 0m23.28s  || +0m00.66s
0m23.52s  | Util/ZUtil                                                   | 0m22.27s  || +0m00.25s
0m18.63s  | Compilers/Named/ContextProperties/SmartMap                   | 0m17.26s  || +0m00.36s
0m18.44s  | Compilers/Named/ContextProperties/NameUtil                   | 0m17.95s  || +0m00.49s
0m16.18s  | Specific/IntegrationTestMul                                  | 0m16.41s  || -0m00.23s
0m15.14s  | Compilers/Z/ArithmeticSimplifierInterp                       | 0m14.43s  || +0m00.71s
0m14.41s  | Algebra/Field                                                | 0m15.30s  || -0m00.89s
0m14.18s  | Specific/IntegrationTestSquare                               | 0m14.60s  || -0m00.41s
0m14.08s  | Compilers/CommonSubexpressionEliminationWf                   | 0m14.07s  || +0m00.00s
0m13.82s  | Specific/ArithmeticSynthesisTest                             | 0m10.24s  || +0m00.58s
0m13.34s  | Specific/IntegrationTestSub                                  | 0m13.49s  || -0m00.15s
0m11.72s  | Primitives/MxDHRepChange                                     | 0m11.02s  || +0m00.70s
0m11.30s  | Compilers/Z/Bounds/InterpretationLemmas/IsBoundedBy          | 0m11.49s  || -0m00.18s
0m11.17s  | Arithmetic/MontgomeryReduction/Proofs                        | 0m10.42s  || +0m00.75s
0m11.13s  | Compilers/Named/MapCastInterp                                | 0m11.12s  || +0m00.01s
0m10.54s  | LegacyArithmetic/ArchitectureToZLikeProofs                   | 0m11.01s  || -0m00.47s
0m10.21s  | Compilers/InlineWf                                           | 0m11.00s  || -0m00.78s
0m10.21s  | LegacyArithmetic/Double/Proofs/Multiply                      | 0m10.51s  || -0m00.29s
0m10.07s  | Specific/ArithmeticSynthesisTest130                          | 0m06.78s  || +0m00.29s
0m09.96s  | Compilers/Named/RegisterAssignInterp                         | 0m10.03s  || -0m00.06s
0m09.70s  | LegacyArithmetic/Double/Proofs/ShiftRightDoubleWordImmediate | 0m10.77s  || -0m00.07s
0m08.93s  | Arithmetic/Core                                              | 0m08.42s  || +0m00.50s
0m08.87s  | Algebra/Ring                                                 | 0m08.99s  || -0m00.12s
0m08.61s  | Util/FixedWordSizesEquality                                  | 0m08.39s  || +0m00.21s
0m08.15s  | LegacyArithmetic/Double/Proofs/SpreadLeftImmediate           | 0m08.99s  || -0m00.83s
0m07.97s  | Bedrock/Word                                                 | 0m07.77s  || +0m00.20s
0m07.92s  | Compilers/LinearizeWf                                        | 0m08.05s  || -0m00.13s
0m07.04s  | Util/ListUtil                                                | 0m06.56s  || +0m00.48s
0m06.78s  | Curves/Edwards/Pre                                           | 0m06.90s  || -0m00.12s
0m06.76s  | LegacyArithmetic/Pow2BaseProofs                              | 0m06.88s  || -0m00.12s
0m06.60s  | LegacyArithmetic/Double/Proofs/RippleCarryAddSub             | 0m06.60s  || +0m00.00s
0m05.80s  | Algebra/Field_test                                           | 0m06.11s  || -0m00.31s
0m04.49s  | Compilers/EtaWf                                              | 0m04.42s  || +0m00.07s
0m04.39s  | Util/ForLoop/Unrolling                                       | 0m04.52s  || -0m00.12s
0m04.32s  | Arithmetic/BarrettReduction/HAC                              | 0m04.39s  || -0m00.06s
0m04.26s  | Compilers/Named/CompileWf                                    | 0m04.50s  || -0m00.24s
0m04.25s  | LegacyArithmetic/InterfaceProofs                             | 0m03.92s  || +0m00.33s
0m04.13s  | Compilers/WfProofs                                           | 0m03.88s  || +0m00.25s
0m04.07s  | Compilers/TestCase                                           | 0m04.19s  || -0m00.12s
0m03.92s  | Arithmetic/Saturated                                         | 0m04.18s  || -0m00.25s
0m03.91s  | Specific/FancyMachine256/Montgomery                          | 0m03.86s  || +0m00.05s
0m03.69s  | LegacyArithmetic/ZBoundedZ                                   | 0m03.43s  || +0m00.25s
0m03.68s  | Curves/Montgomery/Affine                                     | 0m03.38s  || +0m00.30s
0m03.62s  | Arithmetic/ModularArithmeticTheorems                         | 0m03.35s  || +0m00.27s
0m03.51s  | Specific/FancyMachine256/Barrett                             | 0m03.47s  || +0m00.03s
0m03.43s  | Compilers/Named/CompileInterp                                | 0m03.47s  || -0m00.04s
0m03.37s  | Arithmetic/BarrettReduction/Generalized                      | 0m03.49s  || -0m00.12s
0m03.29s  | LegacyArithmetic/Double/Proofs/ShiftLeft                     | 0m04.16s  || -0m00.87s
0m03.27s  | Spec/MontgomeryCurve                                         | 0m03.57s  || -0m00.29s
0m03.26s  | Compilers/Named/ContextProperties                            | 0m03.18s  || +0m00.07s
0m03.12s  | Compilers/InlineInterp                                       | 0m03.16s  || -0m00.04s
0m03.09s  | LegacyArithmetic/Double/Proofs/ShiftRight                    | 0m04.30s  || -0m00.20s
0m02.97s  | LegacyArithmetic/Double/Proofs/Decode                        | 0m03.05s  || -0m00.07s
0m02.89s  | Compilers/Z/Bounds/Relax                                     | 0m02.76s  || +0m00.13s
0m02.86s  | Compilers/Named/NameUtilProperties                           | 0m02.86s  || +0m00.00s
0m02.79s  | Compilers/CommonSubexpressionEliminationProperties           | 0m02.68s  || +0m00.10s
0m02.77s  | Compilers/Z/Bounds/InterpretationLemmas/PullCast             | 0m02.73s  || +0m00.04s
0m02.63s  | LegacyArithmetic/BarretReduction                             | 0m02.50s  || +0m00.12s
0m02.59s  | Specific/FancyMachine256/Core                                | 0m02.21s  || +0m00.37s
0m02.32s  | Util/ForLoop/InvariantFramework                              | 0m02.15s  || +0m00.16s
0m02.28s  | Util/WordUtil                                                | 0m02.36s  || -0m00.08s
0m02.27s  | Compilers/WfReflective                                       | 0m02.19s  || +0m00.08s
0m02.04s  | Spec/WeierstrassCurve                                        | 0m00.61s  || +0m00.43s
0m01.95s  | LegacyArithmetic/MontgomeryReduction                         | 0m01.80s  || +0m00.14s
   N/A    | Curves/Weierstrass/Pre                                       | 0m01.94s  || -0m00.94s
0m01.82s  | Util/NatUtil                                                 | 0m01.80s  || +0m00.02s
0m01.71s  | Arithmetic/BarrettReduction/Wikipedia                        | 0m01.72s  || -0m00.01s
0m01.71s  | Compilers/Z/Bounds/Pipeline/Definition                       | 0m01.52s  || +0m00.18s
0m01.65s  | Util/Tuple                                                   | 0m01.64s  || +0m00.01s
0m01.64s  | Arithmetic/PrimeFieldTheorems                                | 0m01.67s  || -0m00.03s
0m01.59s  | Compilers/Named/InterpretToPHOASWf                           | 0m01.60s  || -0m00.01s
0m01.55s  | Algebra/Group                                                | 0m01.51s  || +0m00.04s
0m01.54s  | Compilers/Z/Syntax/Equality                                  | 0m01.48s  || +0m00.06s
0m01.26s  | Compilers/Relations                                          | 0m01.25s  || +0m00.01s
0m01.18s  | Compilers/LinearizeInterp                                    | 0m01.35s  || -0m00.17s
0m01.13s  | Compilers/WfInversion                                        | 0m01.02s  || +0m00.10s
0m01.09s  | Algebra/IntegralDomain                                       | 0m01.50s  || -0m00.40s
0m01.05s  | Compilers/Named/CompileProperties                            | 0m00.93s  || +0m00.12s
0m01.04s  | Util/NumTheoryUtil                                           | 0m01.01s  || +0m00.03s
0m01.02s  | Compilers/Named/InterpretToPHOASInterp                       | 0m00.90s  || +0m00.12s
0m00.98s  | LegacyArithmetic/Double/Proofs/BitwiseOr                     | 0m00.95s  || +0m00.03s
0m00.97s  | Util/PartiallyReifiedProp                                    | 0m00.93s  || +0m00.03s
0m00.97s  | LegacyArithmetic/Double/Proofs/LoadImmediate                 | 0m01.09s  || -0m00.12s
0m00.93s  | Specific/IntegrationTestTemporaryMiscCommon                  | 0m00.86s  || +0m00.07s
0m00.86s  | Compilers/Z/CNotations                                       | 0m00.82s  || +0m00.04s
0m00.85s  | Arithmetic/Karatsuba                                         | 0m00.87s  || -0m00.02s
0m00.85s  | Compilers/Z/Syntax/Util                                      | 0m00.75s  || +0m00.09s
0m00.84s  | LegacyArithmetic/BaseSystemProofs                            | 0m00.89s  || -0m00.05s
0m00.80s  | Compilers/MapCastByDeBruijnInterp                            | 0m00.99s  || -0m00.18s
0m00.78s  | Compilers/MultiSizeTest                                      | 0m00.78s  || +0m00.00s
0m00.75s  | Util/IterAssocOp                                             | 0m00.70s  || +0m00.05s
0m00.74s  | Util/ZUtil/Stabilization                                     | 0m00.74s  || +0m00.00s
0m00.73s  | LegacyArithmetic/Interface                                   | 0m00.64s  || +0m00.08s
0m00.67s  | Compilers/WfReflectiveGen                                    | 0m00.62s  || +0m00.05s
0m00.67s  | Util/CPSUtil                                                 | 0m00.58s  || +0m00.09s
0m00.67s  | Compilers/Z/Bounds/Pipeline/ReflectiveTactics                | 0m00.70s  || -0m00.02s
0m00.67s  | Curves/Montgomery/XZ                                         | 0m00.57s  || +0m00.10s
0m00.66s  | Compilers/MapCastByDeBruijnWf                                | 0m00.71s  || -0m00.04s
0m00.64s  | Compilers/InterpByIsoProofs                                  | 0m00.60s  || +0m00.04s
0m00.63s  | Compilers/Z/JavaNotations                                    | 0m00.62s  || +0m00.01s
0m00.62s  | Arithmetic/ModularArithmeticPre                              | 0m00.54s  || +0m00.07s
0m00.61s  | Spec/CompleteEdwardsCurve                                    | 0m00.60s  || +0m00.01s
0m00.60s  | Util/HList                                                   | 0m00.53s  || +0m00.06s
0m00.59s  | Util/Decidable                                               | 0m00.63s  || -0m00.04s
0m00.59s  | Compilers/CommonSubexpressionEliminationInterp               | 0m00.80s  || -0m00.21s
0m00.58s  | Compilers/Z/CommonSubexpressionElimination                   | 0m00.54s  || +0m00.03s
0m00.58s  | LegacyArithmetic/Double/Proofs/SelectConditional             | 0m00.90s  || -0m00.32s
0m00.57s  | Compilers/InterpWfRel                                        | 0m00.60s  || -0m00.03s
0m00.57s  | Compilers/Named/AListContext                                 | 0m00.53s  || +0m00.03s
0m00.57s  | Util/AdditionChainExponentiation                             | 0m00.51s  || +0m00.05s
0m00.56s  | Compilers/Z/Bounds/RoundUpLemmas                             | 0m00.59s  || -0m00.02s
0m00.56s  | Compilers/InputSyntax                                        | 0m00.54s  || +0m00.02s
0m00.55s  | Compilers/Named/FMapContext                                  | 0m00.55s  || +0m00.00s
0m00.55s  | Curves/Weierstrass/Affine                                    | 0m00.61s  || -0m00.05s
0m00.54s  | Spec/EdDSA                                                   | 0m00.53s  || +0m00.01s
0m00.54s  | Compilers/Z/Bounds/Pipeline                                  | 0m00.55s  || -0m00.01s
0m00.53s  | Compilers/Z/Bounds/InterpretationLemmas/Tactics              | 0m00.45s  || +0m00.08s
0m00.53s  | LegacyArithmetic/Double/Core                                 | 0m00.51s  || +0m00.02s
0m00.53s  | Compilers/CommonSubexpressionElimination                     | 0m00.51s  || +0m00.02s
0m00.51s  | Util/NUtil                                                   | 0m00.53s  || -0m00.02s
0m00.51s  | LegacyArithmetic/Double/Proofs/ShiftLeftRightTactic          | 0m00.47s  || +0m00.04s
0m00.51s  | Util/ForLoop/Tests                                           | 0m00.45s  || +0m00.06s
0m00.51s  | Compilers/Z/Reify                                            | 0m00.52s  || -0m00.01s
0m00.51s  | Compilers/Z/Bounds/MapCastByDeBruijnInterp                   | 0m00.50s  || +0m00.01s
0m00.50s  | LegacyArithmetic/ZBounded                                    | 0m00.51s  || -0m00.01s
0m00.50s  | Compilers/Z/ArithmeticSimplifier                             | 0m00.47s  || +0m00.03s
0m00.50s  | LegacyArithmetic/ArchitectureToZLike                         | 0m00.49s  || +0m00.01s
0m00.49s  | Compilers/InterpWf                                           | 0m00.49s  || +0m00.00s
0m00.49s  | Compilers/Z/Bounds/Interpretation                            | 0m00.47s  || +0m00.02s
0m00.48s  | Specific/IntegrationTestDisplayCommon                        | 0m00.45s  || +0m00.02s
0m00.47s  | Spec/ModularArithmetic                                       | 0m00.41s  || +0m00.06s
0m00.47s  | Compilers/Z/Bounds/MapCastByDeBruijn                         | 0m00.47s  || +0m00.00s
0m00.47s  | Compilers/Z/Bounds/Pipeline/Glue                             | 0m00.49s  || -0m00.02s
0m00.46s  | Algebra/Nsatz                                                | 0m00.62s  || -0m00.15s
0m00.46s  | Compilers/Reify                                              | 0m00.45s  || +0m00.01s
0m00.46s  | Compilers/Z/CommonSubexpressionEliminationWf                 | 0m00.48s  || -0m00.01s
0m00.46s  | Compilers/Z/MapCastByDeBruijnInterp                          | 0m00.47s  || -0m00.00s
0m00.46s  | Compilers/Z/Bounds/MapCastByDeBruijnWf                       | 0m00.49s  || -0m00.02s
0m00.45s  | LegacyArithmetic/BaseSystem                                  | 0m00.44s  || +0m00.01s
0m00.45s  | Util/ZRange                                                  | 0m00.44s  || +0m00.01s
0m00.45s  | Util/BoundedWord                                             | 0m00.43s  || +0m00.02s
0m00.44s  | Util/Factorize                                               | 0m00.57s  || -0m00.12s
0m00.44s  | Compilers/Z/Syntax                                           | 0m00.44s  || +0m00.00s
0m00.44s  | Compilers/Z/CommonSubexpressionEliminationInterp             | 0m00.59s  || -0m00.14s
0m00.44s  | Compilers/Z/MapCastByDeBruijnWf                              | 0m00.45s  || -0m00.01s
0m00.43s  | Compilers/Z/Inline                                           | 0m00.39s  || +0m00.03s
0m00.43s  | Compilers/Named/PositiveContext/DefaultsProperties           | 0m00.44s  || -0m00.01s
0m00.42s  | Compilers/Z/HexNotationConstants                             | 0m00.43s  || -0m00.01s
0m00.42s  | LegacyArithmetic/Pow2Base                                    | 0m00.42s  || +0m00.00s
0m00.42s  | Compilers/Z/FoldTypes                                        | 0m00.38s  || +0m00.03s
0m00.42s  | Compilers/Z/InlineInterp                                     | 0m00.40s  || +0m00.01s
0m00.42s  | Compilers/Z/MapCastByDeBruijn                                | 0m00.45s  || -0m00.03s
0m00.41s  | Compilers/Tuple                                              | 0m00.41s  || +0m00.00s
0m00.41s  | Compilers/Z/ArithmeticSimplifierUtil                         | 0m00.44s  || -0m00.03s
0m00.40s  | Compilers/Named/DeadCodeElimination                          | 0m00.39s  || +0m00.01s
0m00.39s  | Arithmetic/MontgomeryReduction/Definition                    | 0m00.43s  || -0m00.03s
0m00.39s  | Compilers/Z/Bounds/Pipeline/OutputType                       | 0m00.42s  || -0m00.02s
0m00.39s  | Compilers/Z/InlineWf                                         | 0m00.41s  || -0m00.01s
0m00.38s  | Compilers/Named/EstablishLiveness                            | 0m00.40s  || -0m00.02s
0m00.37s  | Compilers/Z/BinaryNotationConstants                          | 0m00.38s  || -0m00.01s
0m00.37s  | Compilers/Named/WeakListContext                              | 0m00.35s  || +0m00.02s
0m00.36s  | Compilers/FilterLive                                         | 0m00.36s  || +0m00.00s
0m00.36s  | Algebra/ScalarMult                                           | 0m00.33s  || +0m00.02s
0m00.35s  | Bedrock/Nomega                                               | 0m00.39s  || -0m00.04s
0m00.34s  | Util/FixedWordSizes                                          | 0m00.34s  || +0m00.00s
0m00.34s  | Compilers/Named/WfInterp                                     | 0m00.32s  || +0m00.02s
0m00.34s  | Compilers/Named/PositiveContext                              | 0m00.33s  || +0m00.01s
0m00.33s  | Compilers/ExprInversion                                      | 0m00.32s  || +0m00.01s
0m00.32s  | Util/ForLoop/Instances                                       | 0m00.34s  || -0m00.02s
0m00.32s  | Algebra/Monoid                                               | 0m00.29s  || +0m00.03s
0m00.31s  | Compilers/Equality                                           | 0m00.29s  || +0m00.02s
0m00.31s  | Compilers/Z/OpInversion                                      | 0m00.38s  || -0m00.07s
0m00.31s  | Compilers/Named/RegisterAssign                               | 0m00.32s  || -0m00.01s
0m00.31s  | Compilers/MapCastByDeBruijn                                  | 0m00.31s  || +0m00.00s
0m00.30s  | Algebra/Hierarchy                                            | 0m00.32s  || -0m00.02s
0m00.30s  | Compilers/Named/PositiveContext/Defaults                     | 0m00.29s  || +0m00.01s
0m00.29s  | Util/Sum                                                     | 0m00.30s  || -0m00.01s
0m00.29s  | Spec/MxDH                                                    | 0m00.26s  || +0m00.02s
0m00.28s  | Compilers/SmartMap                                           | 0m00.28s  || +0m00.00s
0m00.27s  | Compilers/EtaInterp                                          | 0m00.26s  || +0m00.01s
0m00.26s  | Compilers/Named/ContextDefinitions                           | 0m00.22s  || +0m00.04s
0m00.24s  | Compilers/CommonSubexpressionEliminationDenote               | 0m00.24s  || +0m00.00s
0m00.23s  | Util/ForLoop                                                 | 0m00.22s  || +0m00.01s
0m00.23s  | Compilers/Named/ContextOn                                    | 0m00.25s  || -0m00.01s
0m00.21s  | Util/LetInMonad                                              | 0m00.20s  || +0m00.00s
0m00.21s  | Compilers/Named/ContextProperties/Tactics                    | 0m00.23s  || -0m00.02s
0m00.20s  | Compilers/InterpProofs                                       | 0m00.22s  || -0m00.01s
0m00.17s  | Util/Sigma                                                   | 0m00.10s  || +0m00.07s
0m00.17s  | Compilers/RewriterWf                                         | 0m00.14s  || +0m00.03s
0m00.15s  | Util/Option                                                  | 0m00.16s  || -0m00.01s
0m00.14s  | Compilers/Named/Compile                                      | 0m00.13s  || +0m00.01s
0m00.13s  | Compilers/Wf                                                 | 0m00.14s  || -0m00.01s
0m00.12s  | Util/Relations                                               | 0m00.12s  || +0m00.00s
0m00.11s  | Compilers/Named/NameUtil                                     | 0m00.12s  || -0m00.00s
0m00.11s  | Compilers/Conversion                                         | 0m00.12s  || -0m00.00s
0m00.11s  | Compilers/Named/IdContext                                    | 0m00.11s  || +0m00.00s
0m00.10s  | Util/Equality                                                | 0m00.10s  || +0m00.00s
0m00.10s  | Util/Prod                                                    | 0m00.10s  || +0m00.00s
0m00.10s  | Util/PointedProp                                             | 0m00.11s  || -0m00.00s
0m00.09s  | Compilers/TypeInversion                                      | 0m00.09s  || +0m00.00s
0m00.09s  | Compilers/Named/MapCast                                      | 0m00.07s  || +0m00.01s
0m00.07s  | Compilers/Syntax                                             | 0m00.05s  || +0m00.02s
0m00.07s  | Compilers/Linearize                                          | 0m00.06s  || +0m00.01s
0m00.06s  | Util/HProp                                                   | 0m00.05s  || +0m00.00s
0m00.06s  | Util/Bool                                                    | 0m00.06s  || +0m00.00s
0m00.06s  | Util/Tower                                                   | 0m00.03s  || +0m00.03s
0m00.06s  | Util/Tactics/BreakMatch                                      | 0m00.03s  || +0m00.03s
0m00.06s  | Util/LetIn                                                   | 0m00.05s  || +0m00.00s
0m00.06s  | Compilers/Inline                                             | 0m00.06s  || +0m00.00s
0m00.06s  | Compilers/RewriterInterp                                     | 0m00.06s  || +0m00.00s
0m00.06s  | Compilers/Named/Syntax                                       | 0m00.06s  || +0m00.00s
0m00.06s  | Compilers/Named/Wf                                           | 0m00.05s  || +0m00.00s
0m00.06s  | Compilers/Named/SmartMap                                     | 0m00.06s  || +0m00.00s
0m00.06s  | Compilers/Eta                                                | 0m00.06s  || +0m00.00s
0m00.06s  | Compilers/FoldTypes                                          | 0m00.06s  || +0m00.00s
0m00.06s  | Compilers/InterpByIso                                        | 0m00.05s  || +0m00.00s
0m00.06s  | Compilers/Named/InterpretToPHOAS                             | 0m00.07s  || -0m00.01s
0m00.05s  | Compilers/Map                                                | 0m00.03s  || +0m00.02s
0m00.05s  | Compilers/Rewriter                                           | 0m00.04s  || +0m00.01s
0m00.04s  | Util/Tactics/DebugPrint                                      | 0m00.04s  || +0m00.00s
0m00.04s  | Util/Isomorphism                                             | 0m00.05s  || -0m00.01s
0m00.04s  | Util/Tactics/Test                                            | 0m00.04s  || +0m00.00s
0m00.04s  | Util/Tactics/ConvoyDestruct                                  | 0m00.03s  || +0m00.01s
0m00.04s  | Util/Tactics/DestructTrivial                                 | 0m00.02s  || +0m00.02s
0m00.04s  | Util/Tactics/ETransitivity                                   | 0m00.03s  || +0m00.01s
0m00.04s  | Util/Curry                                                   | 0m00.03s  || +0m00.01s
0m00.04s  | Util/Sigma/Associativity                                     | 0m00.03s  || +0m00.01s
0m00.04s  | LegacyArithmetic/VerdiTactics                                | 0m00.03s  || +0m00.01s
0m00.04s  | Util/Tactics/Head                                            | 0m00.04s  || +0m00.00s
0m00.04s  | Util/Tactics/Not                                             | 0m00.02s  || +0m00.02s
0m00.04s  | Util/Tactics/UniquePose                                      | 0m00.03s  || +0m00.01s
0m00.04s  | Util/Tactics/DestructHead                                    | 0m00.03s  || +0m00.01s
0m00.04s  | Compilers/TypeUtil                                           | 0m00.03s  || +0m00.01s
0m00.04s  | Util/AutoRewrite                                             | 0m00.04s  || +0m00.00s
0m00.04s  | Compilers/CountLets                                          | 0m00.06s  || -0m00.01s
0m00.04s  | Compilers/Named/Context                                      | 0m00.05s  || -0m00.01s
0m00.03s  | Util/GlobalSettings                                          | 0m00.04s  || -0m00.01s
0m00.03s  | Util/Tactics/Revert                                          | 0m00.02s  || +0m00.00s
0m00.03s  | Util/Tactics/Contains                                        | 0m00.03s  || +0m00.00s
0m00.03s  | Util/IffT                                                    | 0m00.06s  || -0m00.03s
0m00.03s  | Util/Tactics/ClearDuplicates                                 | 0m00.03s  || +0m00.00s
0m00.03s  | Util/Tactics/ESpecialize                                     | 0m00.03s  || +0m00.00s
0m00.03s  | Util/Tactics/Forward                                         | 0m00.03s  || +0m00.00s
0m00.03s  | Util/Tactics/PrintContext                                    | 0m00.03s  || +0m00.00s
0m00.03s  | Util/Tactics/SetoidSubst                                     | 0m00.04s  || -0m00.01s
0m00.03s  | Util/Tactics/SideConditionsBeforeToAfter                     | 0m00.03s  || +0m00.00s
0m00.03s  | Util/Tactics/SubstEvars                                      | 0m00.02s  || +0m00.00s
0m00.03s  | Util/Tactics/VM                                              | 0m00.02s  || +0m00.00s
0m00.03s  | Util/Sigma/MapProjections                                    | 0m00.03s  || +0m00.00s
0m00.03s  | Util/ChangeInAll                                             | 0m00.02s  || +0m00.00s
0m00.03s  | Util/Sigma/Lift                                              | 0m00.03s  || +0m00.00s
0m00.03s  | Util/Sumbool                                                 | 0m00.09s  || -0m00.06s
0m00.03s  | Util/FixCoqMistakes                                          | 0m00.03s  || +0m00.00s
0m00.03s  | Util/Tactics/SpecializeBy                                    | 0m00.04s  || -0m00.01s
0m00.03s  | Util/Tactics/DestructHyps                                    | 0m00.02s  || +0m00.00s
0m00.03s  | Util/Tactics/SplitInContext                                  | 0m00.03s  || +0m00.00s
0m00.03s  | Util/Logic                                                   | 0m00.04s  || -0m00.01s
0m00.03s  | Util/Tactics/RewriteHyp                                      | 0m00.03s  || +0m00.00s
0m00.03s  | Util/Tactics/MoveLetIn                                       | 0m00.03s  || +0m00.00s
0m00.03s  | Util/Tactics                                                 | 0m00.04s  || -0m00.01s
0m00.03s  | Compilers/RenameBinders                                      | 0m00.05s  || -0m00.02s
0m00.02s  | Util/Tactics/OnSubterms                                      | 0m00.04s  || -0m00.02s
0m00.02s  | Util/Tactics/GetGoal                                         | 0m00.01s  || +0m00.01s
0m00.02s  | Util/Tactics/ChangeInAll                                     | 0m00.04s  || -0m00.02s
0m00.02s  | Util/Tactics/ClearAll                                        | 0m00.04s  || -0m00.02s
0m00.02s  | Util/Tactics/SetEvars                                        | 0m00.03s  || -0m00.00s
0m00.02s  | Util/Tactics/SimplifyRepeatedIfs                             | 0m00.02s  || +0m00.00s
0m00.02s  | Util/Tactics/SubstLet                                        | 0m00.02s  || +0m00.00s
0m00.02s  | Util/Tactics/TransparentAssert                               | 0m00.02s  || +0m00.00s
0m00.02s  | Util/Tactics/UnifyAbstractReflexivity                        | 0m00.03s  || -0m00.00s
0m00.02s  | Util/Logic/ImplAnd                                           | 0m00.03s  || -0m00.00s
0m00.02s  | Util/Unit                                                    | 0m00.06s  || -0m00.03s
0m00.02s  | Util/Tactics/DoWithHyp                                       | 0m00.03s  || -0m00.00s
0m00.02s  | Util/Notations                                               | 0m00.03s  || -0m00.00s
0m00.01s  | Util/Tactics/EvarExists                                      | 0m00.02s  || -0m00.01s
0m00.01s  | Util/Tactics/SimplifyProjections                             | 0m00.03s  || -0m00.01s

3 files changed, 29 insertions, 235 deletions

diff --git a/src/Curves/Weierstrass/Affine.v b/src/Curves/Weierstrass/Affine.v
index 90bb3bdbc..3a48bf998 100644
--- a/src/Curves/Weierstrass/Affine.v
+++ b/src/Curves/Weierstrass/Affine.v
@@ -11,8 +11,10 @@ Module W.
     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
+         | inr tt => inr tt
          end.
-    Next Obligation. destruct P as [[[??]|[]]?]; cbv; trivial; fsatz. Qed.
+    Next Obligation.
+      cbv [W.coordinates]; break_match; trivial; fsatz.
+    Qed.
   End W.
 End W.
\ No newline at end of file
diff --git a/src/Curves/Weierstrass/AffineProofs.v b/src/Curves/Weierstrass/AffineProofs.v
index 81583d88f..be76cee90 100644
--- a/src/Curves/Weierstrass/AffineProofs.v
+++ b/src/Curves/Weierstrass/AffineProofs.v
@@ -18,179 +18,33 @@ Module W.
     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).
 
+    Local Ltac Algebra_split :=
+      repeat match goal with
+             | |- Proper _ _ => cbv [Proper respectful]; intros
+             | |- Equivalence _ => split; [intros ? | intros ??? | intros ????? ]
+             | |- monoid => split
+             | |- group => split
+             | |- abelian_group => split
+             | |- is_associative => split; intros ???
+             | |- is_commutative => split; intros ??
+             | |- is_left_inverse => split; intros ?
+             | |- is_right_inverse => split; intros ?
+             | |- is_left_identity => split; intros ?
+             | |- is_right_identity => split; intros ?
+             end.
+
     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) *)
-
-      (* 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. (* Finished transaction in 390.998 secs (390.783u,0.276s) (successful) *)
+        cbv [W.opp W.eq W.zero W.add W.coordinates proj1_sig];
+          repeat match goal with
+                 | _ => progress Algebra_split
+                 | H: _ /\ _ |- _ => destruct H
+                 | |- _ /\ _ => split
+                 | _ => progress break_match
+                 | _ => progress break_match_hyps
+                 end; try contradiction; trivial.
+      Time par: abstract (fsatz || (cbv [id] in *; fsatz)).
+    Time Qed.
   End W.
 End W.
diff --git a/src/Curves/Weierstrass/Pre.v b/src/Curves/Weierstrass/Pre.v
deleted file mode 100644
index 6647d8e76..000000000
--- a/src/Curves/Weierstrass/Pre.v
+++ /dev/null
@@ -1,62 +0,0 @@
-Require Import Coq.Classes.Morphisms. Require Coq.Setoids.Setoid.
-Require Import Crypto.Algebra.Field.
-Require Import Crypto.Util.Tactics.DestructHead.
-Require Import Crypto.Util.Tactics.BreakMatch.
-Require Import Crypto.Util.Notations.
-Require Import Crypto.Util.Decidable.
-Import BinNums.
-
-Local Open Scope core_scope.
-
-Section Pre.
-  Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}
-          {field:@Algebra.Hierarchy.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))}
-          {eq_dec: DecidableRel Feq}.
-  Local Infix "=" := Feq. Local Notation "a <> b" := (not (a = b)).
-  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 "*" := Fmul.
-  Local Infix "-" := Fsub. Local Infix "/" := Fdiv.
-  Local Notation "- x" := (Fopp x).
-  Local Notation "x ^ 2" := (x*x). Local Notation "x ^ 3" := (x*x^2).
-  Local Notation "'∞'" := unit : type_scope.
-  Local Notation "'∞'" := (inr tt) : core_scope.
-  Local Notation "2" := (1+1). Local Notation "3" := (1+2).
-  Local Notation "( x , y )" := (inl (pair x y)).
-
-  Context {a:F}.
-  Context {b:F}.
-
-  (* the canonical definitions are in Spec *)
-  Let onCurve (P:F*F + ∞) := match P with
-                             | (x, y) => y^2 = x^3 + a*x + b
-                             | ∞ => True
-                             end.
-  Let add (P1' P2':F*F + ∞) : F*F + ∞ :=
-    match P1', P2' return _ with
-    | (x1, y1), (x2, y2) =>
-      if dec (x1 = x2)
-      then
-        if dec (y2 = -y1)
-        then ∞
-        else let k := (3*x1^2+a)/(2*y1) in
-             let x3 := k^2-x1-x1 in
-             let y3 := k*(x1-x3)-y1 in
-             (x3, y3)
-      else let k := (y2-y1)/(x2-x1) in
-           let x3 := k^2-x1-x2 in
-           let y3 := k*(x1-x3)-y1 in
-           (x3, y3)
-    | ∞, ∞ => ∞
-    | ∞, _ => P2'
-    | _, ∞ => P1'
-    end.
-
-  Lemma add_onCurve P1 P2 (_:onCurve P1) (_:onCurve P2) :
-    onCurve (add P1 P2).
-  Proof using a b char_ge_3 eq_dec field.
-    destruct_head' sum; destruct_head' prod;
-      cbv [onCurve add] in *; break_match; trivial; [|]; fsatz.
-  Qed.
-End Pre.