blob: a3e6182bc9fa5f6f6da6753d027c70352b38b358 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
|
Require Import Coq.ZArith.ZArith Coq.omega.Omega.
Require Import Crypto.Util.ZUtil.Hints.Core.
Local Open Scope Z_scope.
Module Z.
Lemma div_abs_sgn_nonneg a b : 0 <= Z.sgn (Z.abs a / Z.abs b).
Proof.
generalize (Zdiv_sgn (Z.abs a) (Z.abs b)).
destruct a, b; simpl; omega.
Qed.
Hint Resolve div_abs_sgn_nonneg : zarith.
End Z.
|
