Library Coq.NArith.Ndec
A boolean equality over N
Notation Peqb :=
Peqb (
only parsing).
Notation Neqb :=
Neqb (
only parsing).
Notation Peqb_correct :=
Peqb_refl (
only parsing).
Lemma Peqb_complete :
forall p p',
Peqb p p' = true ->
p = p'.
Lemma Peqb_Pcompare :
forall p p',
Peqb p p' = true ->
Pcompare p p' Eq = Eq.
Lemma Pcompare_Peqb :
forall p p',
Pcompare p p' Eq = Eq ->
Peqb p p' = true.
Lemma Neqb_correct :
forall n,
Neqb n n = true.
Lemma Neqb_Ncompare :
forall n n',
Neqb n n' = true ->
Ncompare n n' = Eq.
Lemma Ncompare_Neqb :
forall n n',
Ncompare n n' = Eq ->
Neqb n n' = true.
Lemma Neqb_complete :
forall a a',
Neqb a a' = true ->
a = a'.
Lemma Neqb_comm :
forall a a',
Neqb a a' = Neqb a' a.
Lemma Nxor_eq_true :
forall a a',
Nxor a a' = N0 ->
Neqb a a' = true.
Lemma Nxor_eq_false :
forall a a' p,
Nxor a a' = Npos p ->
Neqb a a' = false.
Lemma Nodd_not_double :
forall a,
Nodd a ->
forall a0,
Neqb (
Ndouble a0)
a = false.
Lemma Nnot_div2_not_double :
forall a a0,
Neqb (
Ndiv2 a)
a0 = false ->
Neqb a (
Ndouble a0)
= false.
Lemma Neven_not_double_plus_one :
forall a,
Neven a ->
forall a0,
Neqb (
Ndouble_plus_one a0)
a = false.
Lemma Nnot_div2_not_double_plus_one :
forall a a0,
Neqb (
Ndiv2 a)
a0 = false ->
Neqb (
Ndouble_plus_one a0)
a = false.
Lemma Nbit0_neq :
forall a a',
Nbit0 a = false ->
Nbit0 a' = true ->
Neqb a a' = false.
Lemma Ndiv2_eq :
forall a a',
Neqb a a' = true ->
Neqb (
Ndiv2 a) (
Ndiv2 a')
= true.
Lemma Ndiv2_neq :
forall a a',
Neqb (
Ndiv2 a) (
Ndiv2 a')
= false ->
Neqb a a' = false.
Lemma Ndiv2_bit_eq :
forall a a',
Nbit0 a = Nbit0 a' ->
Ndiv2 a = Ndiv2 a' ->
a = a'.
Lemma Ndiv2_bit_neq :
forall a a',
Neqb a a' = false ->
Nbit0 a = Nbit0 a' ->
Neqb (
Ndiv2 a) (
Ndiv2 a')
= false.
Lemma Nneq_elim :
forall a a',
Neqb a a' = false ->
Nbit0 a = negb (
Nbit0 a')
\/
Neqb (
Ndiv2 a) (
Ndiv2 a')
= false.
Lemma Ndouble_or_double_plus_un :
forall a,
{a0 : N | a = Ndouble a0} + {a1 : N | a = Ndouble_plus_one a1}.
A boolean order on N
Definition Nleb (
a b:
N) :=
leb (
nat_of_N a) (
nat_of_N b).
Lemma Nleb_Nle :
forall a b,
Nleb a b = true <-> Nle a b.
Lemma Nleb_refl :
forall a,
Nleb a a = true.
Lemma Nleb_antisym :
forall a b,
Nleb a b = true ->
Nleb b a = true ->
a = b.
Lemma Nleb_trans :
forall a b c,
Nleb a b = true ->
Nleb b c = true ->
Nleb a c = true.
Lemma Nleb_ltb_trans :
forall a b c,
Nleb a b = true ->
Nleb c b = false ->
Nleb c a = false.
Lemma Nltb_leb_trans :
forall a b c,
Nleb b a = false ->
Nleb b c = true ->
Nleb c a = false.
Lemma Nltb_trans :
forall a b c,
Nleb b a = false ->
Nleb c b = false ->
Nleb c a = false.
Lemma Nltb_leb_weak :
forall a b:
N,
Nleb b a = false ->
Nleb a b = true.
Lemma Nleb_double_mono :
forall a b,
Nleb a b = true ->
Nleb (
Ndouble a) (
Ndouble b)
= true.
Lemma Nleb_double_plus_one_mono :
forall a b,
Nleb a b = true ->
Nleb (
Ndouble_plus_one a) (
Ndouble_plus_one b)
= true.
Lemma Nleb_double_mono_conv :
forall a b,
Nleb (
Ndouble a) (
Ndouble b)
= true ->
Nleb a b = true.
Lemma Nleb_double_plus_one_mono_conv :
forall a b,
Nleb (
Ndouble_plus_one a) (
Ndouble_plus_one b)
= true ->
Nleb a b = true.
Lemma Nltb_double_mono :
forall a b,
Nleb a b = false ->
Nleb (
Ndouble a) (
Ndouble b)
= false.
Lemma Nltb_double_plus_one_mono :
forall a b,
Nleb a b = false ->
Nleb (
Ndouble_plus_one a) (
Ndouble_plus_one b)
= false.
Lemma Nltb_double_mono_conv :
forall a b,
Nleb (
Ndouble a) (
Ndouble b)
= false ->
Nleb a b = false.
Lemma Nltb_double_plus_one_mono_conv :
forall a b,
Nleb (
Ndouble_plus_one a) (
Ndouble_plus_one b)
= false ->
Nleb a b = false.
Lemma Nltb_Ncompare :
forall a b,
Nleb a b = false <-> Ncompare a b = Gt.
Lemma Ncompare_Gt_Nltb :
forall a b,
Ncompare a b = Gt ->
Nleb a b = false.
Lemma Ncompare_Lt_Nltb :
forall a b,
Ncompare a b = Lt ->
Nleb b a = false.
Definition Nmin' (
a b:
N) :=
if Nleb a b then a else b.
Lemma Nmin_Nmin' :
forall a b,
Nmin a b = Nmin' a b.
Lemma Nmin_choice :
forall a b,
{Nmin a b = a} + {Nmin a b = b}.
Lemma Nmin_le_1 :
forall a b,
Nleb (
Nmin a b)
a = true.
Lemma Nmin_le_2 :
forall a b,
Nleb (
Nmin a b)
b = true.
Lemma Nmin_le_3 :
forall a b c,
Nleb a (
Nmin b c)
= true ->
Nleb a b = true.
Lemma Nmin_le_4 :
forall a b c,
Nleb a (
Nmin b c)
= true ->
Nleb a c = true.
Lemma Nmin_le_5 :
forall a b c,
Nleb a b = true ->
Nleb a c = true ->
Nleb a (
Nmin b c)
= true.
Lemma Nmin_lt_3 :
forall a b c,
Nleb (
Nmin b c)
a = false ->
Nleb b a = false.
Lemma Nmin_lt_4 :
forall a b c,
Nleb (
Nmin b c)
a = false ->
Nleb c a = false.