proved feSign_correct

1 files changed, 11 insertions, 1 deletions

diff --git a/src/ModularArithmetic/ModularBaseSystemProofs.v b/src/ModularArithmetic/ModularBaseSystemProofs.v
index f6efdfd87..ef89cb5ae 100644
--- a/src/ModularArithmetic/ModularBaseSystemProofs.v
+++ b/src/ModularArithmetic/ModularBaseSystemProofs.v
@@ -114,7 +114,17 @@ Section FieldOperationProofs.
       pose proof c_pos; omega.
     + apply base_upper_bound_compatible; auto.
   Qed.
-
+(*
+  Lemma parity_decode : forall u x,
+    u ~= x -> Z.odd (F.to_Z x) = Z.odd (nth_default 0 (to_list u) 0).
+  Proof.
+    cbv [rep decode] in *.
+    intros.
+    rewrite <-H.
+    cbv [ModularBaseSystemList.decode].
+    rewrite F.to_Z_of_Z.
+  Qed.
+*)
   Lemma add_rep : forall u v x y, u ~= x -> v ~= y ->
     add u v ~= (x+y)%F.
   Proof.