Add unicode reserved notations

After    | File Name                                         | Before   || Change
------------------------------------------------------------------------------------
3m17.30s | Total                                             | 3m15.15s || +0m02.15s
------------------------------------------------------------------------------------
0m05.13s | WeierstrassCurve/Pre                              | 0m06.46s || -0m01.33s
0m04.64s | CompleteEdwardsCurve/Pre                          | 0m03.48s || +0m01.15s
0m04.39s | ModularArithmetic/Pow2BaseProofs                  | 0m05.95s || -0m01.56s
0m36.30s | CompleteEdwardsCurve/ExtendedCoordinates          | 0m35.39s || +0m00.90s
0m33.32s | Specific/GF25519                                  | 0m33.98s || -0m00.65s
0m16.42s | ModularArithmetic/ModularBaseSystemProofs         | 0m16.07s || +0m00.35s
0m16.08s | CompleteEdwardsCurve/CompleteEdwardsCurveTheorems | 0m16.77s || -0m00.69s
0m11.33s | Experiments/SpecEd25519                           | 0m11.31s || +0m00.01s
0m07.29s | Specific/GF1305                                   | 0m07.25s || +0m00.04s
0m07.17s | Algebra                                           | 0m06.25s || +0m00.92s
0m04.22s | ModularArithmetic/Tutorial                        | 0m04.27s || -0m00.04s
0m03.99s | BaseSystemProofs                                  | 0m03.84s || +0m00.15s
0m03.36s | ModularArithmetic/ModularBaseSystemOpt            | 0m03.35s || +0m00.00s
0m02.83s | Assembly/State                                    | 0m02.73s || +0m00.10s
0m02.51s | Util/ZUtil                                        | 0m02.42s || +0m00.08s
0m02.30s | ModularArithmetic/PrimeFieldTheorems              | 0m01.63s || +0m00.67s
0m01.92s | Experiments/EdDSARefinement                       | 0m01.87s || +0m00.04s
0m01.89s | BaseSystem                                        | 0m01.20s || +0m00.69s
0m01.87s | Assembly/Wordize                                  | 0m01.89s || -0m00.01s
0m01.64s | ModularArithmetic/ModularArithmeticTheorems       | 0m01.61s || +0m00.02s
0m01.61s | Assembly/Pseudize                                 | 0m01.77s || -0m00.15s
0m01.56s | Encoding/PointEncodingPre                         | 0m01.80s || -0m00.24s
0m01.38s | ModularArithmetic/ModularBaseSystemField          | 0m00.90s || +0m00.47s
0m01.15s | ModularArithmetic/ExtendedBaseVector              | 0m01.44s || -0m00.29s
0m01.02s | ModularArithmetic/ExtPow2BaseMulProofs            | 0m00.95s || +0m00.07s
0m00.99s | ModularArithmetic/BarrettReduction/Z              | 0m01.00s || -0m00.01s
0m00.99s | Encoding/ModularWordEncodingPre                   | 0m00.62s || +0m00.37s
0m00.98s | ModularArithmetic/ModularBaseSystemList           | 0m00.90s || +0m00.07s
0m00.96s | Assembly/Pipeline                                 | 0m00.65s || +0m00.30s
0m00.93s | Util/AdditionChainExponentiation                  | 0m00.62s || +0m00.31s
0m00.92s | Spec/EdDSA                                        | 0m00.61s || +0m00.31s
0m00.91s | Experiments/DerivationsOptionRectLetInEncoding    | 0m00.92s || -0m00.01s
0m00.90s | Util/NumTheoryUtil                                | 0m00.89s || +0m00.01s
0m00.89s | ModularArithmetic/ModularBaseSystemListProofs     | 0m00.94s || -0m00.04s
0m00.88s | Assembly/Pseudo                                   | 0m00.63s || +0m00.25s
0m00.87s | Assembly/QhasmEvalCommon                          | 0m00.83s || +0m00.04s
0m00.78s | Assembly/StringConversion                         | 0m00.54s || +0m00.24s
0m00.71s | Experiments/SpecificCurve25519                    | 0m00.73s || -0m00.02s
0m00.69s | Util/IterAssocOp                                  | 0m00.73s || -0m00.04s
0m00.68s | Assembly/AlmostQhasm                              | 0m00.55s || +0m00.13s
0m00.68s | Assembly/PseudoConversion                         | 0m00.73s || -0m00.04s
0m00.67s | ModularArithmetic/PseudoMersenneBaseParamProofs   | 0m00.63s || +0m00.04s
0m00.67s | ModularArithmetic/Pre                             | 0m00.45s || +0m00.22s
0m00.64s | Testbit                                           | 0m00.90s || -0m00.26s
0m00.64s | Encoding/ModularWordEncodingTheorems              | 0m00.67s || -0m00.03s
0m00.63s | Spec/ModularWordEncoding                          | 0m00.83s || -0m00.19s
0m00.59s | ModularArithmetic/ModularBaseSystem               | 0m00.56s || +0m00.02s
0m00.53s | Spec/ModularArithmetic                            | 0m00.47s || +0m00.06s
0m00.53s | Assembly/Qhasm                                    | 0m00.55s || -0m00.02s
0m00.52s | ModularArithmetic/Pow2Base                        | 0m00.41s || +0m00.11s
0m00.51s | Assembly/QhasmUtil                                | 0m00.45s || +0m00.06s
0m00.49s | Assembly/AlmostConversion                         | 0m00.49s || +0m00.00s
0m00.48s | Assembly/Vectorize                                | 0m00.70s || -0m00.21s
0m00.46s | Spec/WeierstrassCurve                             | 0m00.70s || -0m00.23s
0m00.43s | Spec/CompleteEdwardsCurve                         | 0m00.43s || +0m00.00s
0m00.40s | ModularArithmetic/PseudoMersenneBaseParams        | 0m00.40s || +0m00.00s
0m00.03s | Util/Notations                                    | 0m00.04s || -0m00.01s

1 files changed, 2 insertions, 0 deletions

diff --git a/src/Util/Notations.v b/src/Util/Notations.v
index b23fe37ac..222f63498 100644
--- a/src/Util/Notations.v
+++ b/src/Util/Notations.v
@@ -24,7 +24,9 @@ Reserved Infix "&" (at level 50).
 Reserved Infix "∣" (at level 50).
 Reserved Infix "~=" (at level 70).
 Reserved Infix "==" (at level 70, no associativity).
+Reserved Infix "≡" (at level 70, no associativity).
 Reserved Notation "a !== b" (at level 70, no associativity).
+Reserved Notation "a ≢ b" (at level 70, no associativity).
 Reserved Notation "$$ v" (at level 40).
 Reserved Notation "% A" (at level 20, right associativity).
 Reserved Notation "$ A" (at level 20, right associativity).