diff options
| -rw-r--r-- | src/Util/ZUtil.v | 16 |
1 files changed, 16 insertions, 0 deletions
diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v index 370628b3c..d0aa12e58 100644 --- a/src/Util/ZUtil.v +++ b/src/Util/ZUtil.v @@ -984,6 +984,22 @@ Module Z. Qed. Hint Rewrite Z.div_mul_skip Z.div_mul_skip' using lia : zsimplify. + + Lemma div_small_neg x y : 0 < -x < y -> x / y = -1. + Proof. + intro H; rewrite <- (Z.opp_involutive x). + rewrite Z.div_opp_l_complete by lia. + generalize dependent (-x); clear x; intros x H. + autorewrite with zsimplify; break_match; lia. + Qed. + Hint Rewrite div_small_neg using lia : zsimplify. + + Lemma div_sub_small x y z : 0 <= x < z -> 0 <= y < z -> (x - y) / z = if x <? y then -1 else 0. + Proof. + pose proof (Zlt_cases x y). + intros; break_match; autorewrite with zsimplify; lia. + Qed. + Hint Rewrite div_small_neg using lia : zsimplify. End Z. Module Export BoundsTactics. |