From 29e0fe0bbd09c0044957c7ed05df2227f1fda031 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sun, 15 Oct 2017 11:29:10 -0400 Subject: Add sz2'_nonzero --- src/Specific/Framework/ArithmeticSynthesis/Base.v | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/src/Specific/Framework/ArithmeticSynthesis/Base.v b/src/Specific/Framework/ArithmeticSynthesis/Base.v index 81aff8dea..7c2def910 100644 --- a/src/Specific/Framework/ArithmeticSynthesis/Base.v +++ b/src/Specific/Framework/ArithmeticSynthesis/Base.v @@ -47,6 +47,11 @@ Section gen. Definition m_enc' := Positional.encode (modulo:=modulo) (div:=div) (n:=sz) wt (Z.pos m). + Lemma sz2'_nonzero + (sz_nonzero : sz <> 0%nat) + : sz2' <> 0%nat. + Proof. clear -sz_nonzero; cbv [sz2']; omega. Qed. + Local Ltac Q_cbv := cbv [wt_gen Qround.Qceiling QArith_base.Qmult QArith_base.Qdiv QArith_base.inject_Z QArith_base.Qden QArith_base.Qnum QArith_base.Qopp Qround.Qfloor QArith_base.Qinv QArith_base.Qle Z.of_nat]. Lemma wt_gen0_1 : wt 0 = 1. -- cgit v1.2.3