diff options
Diffstat (limited to 'src/Specific/X25519/C64/ArithmeticSynthesisTest.v')
| -rw-r--r-- | src/Specific/X25519/C64/ArithmeticSynthesisTest.v | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/Specific/X25519/C64/ArithmeticSynthesisTest.v b/src/Specific/X25519/C64/ArithmeticSynthesisTest.v index f4ef43f20..6994e13be 100644 --- a/src/Specific/X25519/C64/ArithmeticSynthesisTest.v +++ b/src/Specific/X25519/C64/ArithmeticSynthesisTest.v @@ -52,6 +52,8 @@ Section Ops. Lemma sz_nonzero : sz <> 0%nat. Proof. vm_decide. Qed. Lemma wt_nonzero i : wt i <> 0. Proof. eapply pow_ceil_mul_nat_nonzero; vm_decide. Qed. + Lemma wt_nonneg i : 0 <= wt i. + Proof. apply pow_ceil_mul_nat_nonneg; vm_decide. Qed. Lemma wt_divides i : wt (S i) / wt i > 0. Proof. apply pow_ceil_mul_nat_divide; vm_decide. Qed. Lemma wt_divides' i : wt (S i) / wt i <> 0. |