From 373fa5249091ea77605454542ed786ca943a758e Mon Sep 17 00:00:00 2001 From: jadep Date: Sun, 30 Oct 2016 13:56:00 -0400 Subject: remove commented-out lemma --- src/ModularArithmetic/ModularBaseSystemProofs.v | 12 +----------- 1 file changed, 1 insertion(+), 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. -- cgit v1.2.3