From cf0d84fea542257e342c47e5046c1237a8c8203a Mon Sep 17 00:00:00 2001 From: Jade Philipoom Date: Fri, 6 Apr 2018 12:50:04 +0200 Subject: prove stronger bound on quotient error for barrett reduction --- src/Util/ZUtil/Div.v | 6 ++++++ 1 file changed, 6 insertions(+) (limited to 'src/Util/ZUtil') 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. -- cgit v1.2.3