blob: ab7767de773d8cb40580044ed4e5ee4f3b603559 (
plain)
1
2
3
4
5
6
7
8
9
|
Require Import Coq.ZArith.ZArith.
Require Import Coq.micromega.Lia.
Local Open Scope Z_scope.
Module Z.
Lemma positive_is_nonzero : forall x, x > 0 -> x <> 0.
Proof. intros; omega. Qed.
Hint Resolve positive_is_nonzero : zarith.
End Z.
|