# Library Coq.omega.Omega

Require Export ZArith_base.
Require Export OmegaLemmas.
Require Export PreOmega.
Hint Resolve Zle_refl Zplus_comm Zplus_assoc Zmult_comm Zmult_assoc Zplus_0_l
Zplus_0_r Zmult_1_l Zplus_opp_l Zplus_opp_r Zmult_plus_distr_l
Zmult_plus_distr_r: zarith.
Require Export Zhints.
Hint Extern 10 (_ = _ :> nat) => abstract omega: zarith.
Hint Extern 10 (_ <= _) => abstract omega: zarith.
Hint Extern 10 (_ < _) => abstract omega: zarith.
Hint Extern 10 (_ >= _) => abstract omega: zarith.
Hint Extern 10 (_ > _) => abstract omega: zarith.
Hint Extern 10 (_ <> _ :> nat) => abstract omega: zarith.
Hint Extern 10 (~ _ <= _) => abstract omega: zarith.
Hint Extern 10 (~ _ < _) => abstract omega: zarith.
Hint Extern 10 (~ _ >= _) => abstract omega: zarith.
Hint Extern 10 (~ _ > _) => abstract omega: zarith.
Hint Extern 10 (_ = _ :> Z) => abstract omega: zarith.
Hint Extern 10 (_ <= _)%Z => abstract omega: zarith.
Hint Extern 10 (_ < _)%Z => abstract omega: zarith.
Hint Extern 10 (_ >= _)%Z => abstract omega: zarith.
Hint Extern 10 (_ > _)%Z => abstract omega: zarith.
Hint Extern 10 (_ <> _ :> Z) => abstract omega: zarith.
Hint Extern 10 (~ (_ <= _)%Z) => abstract omega: zarith.
Hint Extern 10 (~ (_ < _)%Z) => abstract omega: zarith.
Hint Extern 10 (~ (_ >= _)%Z) => abstract omega: zarith.
Hint Extern 10 (~ (_ > _)%Z) => abstract omega: zarith.
Hint Extern 10 False => abstract omega: zarith.