# Library CoLoR.Util.Nat.BigNUtil

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

Set Implicit Arguments.

decidability of equality

Lemma eq_digits_dec : forall x y : digits, {x=y}+{~x=y}.

Lemma eq_int31_dec : forall x y : int31, {x=y}+{~x=y}.

Ltac bad_case := right; intro; inversion H; contr.
Ltac case_tac x y := case (eq_digits_dec x y); [idtac|bad_case].

Import BigN.

Definition w0 := Cyclic31.Int31Cyclic.t.

Lemma eq_BigN_w0_dec : forall x y : w0, {x=y}+{~x=y}.

Lemma eq_BigN_w1_dec : forall x y : w1, {x=y}+{~x=y}.

Lemma eq_BigN_w2_dec : forall x y : w2, {x=y}+{~x=y}.

Lemma eq_BigN_w3_dec : forall x y : w3, {x=y}+{~x=y}.

Lemma eq_BigN_w4_dec : forall x y : w4, {x=y}+{~x=y}.

Lemma eq_BigN_w5_dec : forall x y : w5, {x=y}+{~x=y}.

Lemma eq_BigN_w6_dec : forall x y : w6, {x=y}+{~x=y}.

Section zn2z.

Variables (w : Type) (eq_dec : forall x y : w, {x=y}+{~x=y}).

Lemma eq_zn2z_dec : forall x y : zn2z w, {x=y}+{~x=y}.

End zn2z.

Section word.

Variables (w : Type) (eq_dec : forall x y : w, {x=y}+{~x=y}).

Lemma eq_word_dec : forall n, forall x y : word w n, {x=y}+{~x=y}.

End word.

Lemma eq_bigN_dec : forall x y : bigN, {x=y}+{~x=y}.

properties of ?= on BigN

Open Scope bigN_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).

decidability of comparison

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