remove commented-out lemma

1 files changed, 1 insertions, 11 deletions

diff --git a/src/ModularArithmetic/ModularBaseSystemProofs.v b/src/ModularArithmetic/ModularBaseSystemProofs.v
index ef89cb5ae..f6efdfd87 100644
--- a/src/ModularArithmetic/ModularBaseSystemProofs.v
+++ b/src/ModularArithmetic/ModularBaseSystemProofs.v
@@ -114,17 +114,7 @@ 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.