diff options
| author |  Jade Philipoom <jadep@google.com> | 2018-04-06 12:50:04 +0200 |
|---|---|---|
| committer |  jadephilipoom <jade.philipoom@gmail.com> | 2018-04-11 03:56:21 -0400 |
| commit | cf0d84fea542257e342c47e5046c1237a8c8203a (patch) | |
| tree | 911c9e859d02b7bcbab99276e356cee3ae8eb6e3 /src/Util/ZUtil | |
| parent | ccc79730a7585a3ce952c27d347b194562f4f473 (diff) | |
prove stronger bound on quotient error for barrett reduction
Diffstat (limited to 'src/Util/ZUtil')
| -rw-r--r-- | src/Util/ZUtil/Div.v | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/src/Util/ZUtil/Div.v b/src/Util/ZUtil/Div.v index c596dbab3..f71598446 100644 --- a/src/Util/ZUtil/Div.v +++ b/src/Util/ZUtil/Div.v @@ -159,4 +159,10 @@ Module Z. intros. rewrite Z.add_comm, div_add_mod_cond_l by auto. repeat (f_equal; try ring). Qed. + Lemma div_le_zero x y : 0 < y -> x / y <= 0 -> x < y. + Proof. + clear. intros. + apply Z.nle_gt; intro. + pose proof (Z.div_str_pos x y ltac:(lia)). lia. + Qed. End Z. |