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.