Library CoLoR.Util.Integer.BigZUtil

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
  • Frederic Blanqui, 2009-03-18
extension of BigZ

Set Implicit Arguments.


Lemma eq_bigZ_dec : forall x y : bigZ, {x=y}+{~x=y}.


Open Scope bigZ_scope.

Lemma compare_antisym : forall x y, CompOpp (x?=y) = (y?=x).


Lemma compare_antisym_eq : forall x y c, (x?=y = CompOpp c) <-> (y?=x = c).

Lemma le_gt_dec : forall n m, {n <= m} + {n > m}.