diff options
Diffstat (limited to 'src/Util/ZUtil.v')
-rw-r--r-- | src/Util/ZUtil.v | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v index d0aa12e58..00e227e2d 100644 --- a/src/Util/ZUtil.v +++ b/src/Util/ZUtil.v @@ -990,16 +990,17 @@ Module Z. 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. + autorewrite with zsimplify; edestruct Z_zerop; 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. + (destruct (x <? y) eqn:?); + intros; autorewrite with zsimplify; lia. Qed. - Hint Rewrite div_small_neg using lia : zsimplify. + Hint Rewrite div_sub_small using lia : zsimplify. End Z. Module Export BoundsTactics. |