blob: 3cc18241bc91e4ad33683523b11e22cb3d85cb13 (
plain)
1
2
3
4
5
6
7
8
9
10
11
|
Require Import Coq.ZArith.ZArith.
Require Import Coq.micromega.Lia.
Require Import Crypto.Util.ZUtil.Hints.Core.
Require Import Crypto.Util.ZUtil.ZSimplify.Core.
Local Open Scope Z_scope.
Module Z.
Lemma opp_eq_0_iff a : -a = 0 <-> a = 0.
Proof. omega. Qed.
Hint Rewrite opp_eq_0_iff : zsimplify.
End Z.
|
