diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-10-15 11:29:10 -0400 |
|---|---|---|
| committer |  Jason Gross <jasongross9@gmail.com> | 2017-10-18 23:01:29 -0400 |
| commit | 29e0fe0bbd09c0044957c7ed05df2227f1fda031 (patch) | |
| tree | 22c99584fa7a1f25e015667f884b595f59b9e867 | |
| parent | fd2935407d6dfd5075a49dc44d00b54af0ef70fa (diff) | |
Add sz2'_nonzero
| -rw-r--r-- | src/Specific/Framework/ArithmeticSynthesis/Base.v | 5 |
1 files changed, 5 insertions, 0 deletions
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. |