Ndec.v

Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.

(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

Require Import Bool.
Require Import Sumbool.
Require Import Arith.
Require Import BinPos.
Require Import BinNat.
Require Import Pnat.
Require Import Nnat.
Require Import Ndigits.

Local Open Scope N_scope.

Obsolete results about boolean comparisons over N, kept for compatibility with IntMap and SMC.

Notation Peqb_correct := Pos.eqb_refl (only parsing).
Notation Neqb_correct := N.eqb_refl (only parsing).
Notation Neqb_comm := N.eqb_sym (only parsing).

Lemma Peqb_complete p p' : Pos.eqb p p' = true -> p = p'.p, p':positive
(p =? p')%positive = true -> p = p'
Proof.p, p':positive
(p =? p')%positive = true -> p = p' now apply Pos.eqb_eq. Qed.

Lemma Peqb_Pcompare p p' : Pos.eqb p p' = true -> Pos.compare p p' = Eq.p, p':positive
(p =? p')%positive = true -> (p ?= p')%positive = Eq
Proof.p, p':positive
(p =? p')%positive = true -> (p ?= p')%positive = Eq now rewrite Pos.compare_eq_iff, <- Pos.eqb_eq. Qed.

Lemma Pcompare_Peqb p p' : Pos.compare p p' = Eq -> Pos.eqb p p' = true.p, p':positive
(p ?= p')%positive = Eq -> (p =? p')%positive = true
Proof.p, p':positive
(p ?= p')%positive = Eq -> (p =? p')%positive = true now rewrite Pos.eqb_eq, <- Pos.compare_eq_iff. Qed.

Lemma Neqb_Ncompare n n' : N.eqb n n' = true -> N.compare n n' = Eq.n, n':N
(n =? n') = true -> (n ?= n') = Eq
Proof.n, n':N
(n =? n') = true -> (n ?= n') = Eq now rewrite N.compare_eq_iff, <- N.eqb_eq. Qed.

Lemma Ncompare_Neqb n n' : N.compare n n' = Eq -> N.eqb n n' = true.n, n':N
(n ?= n') = Eq -> (n =? n') = true
Proof.n, n':N
(n ?= n') = Eq -> (n =? n') = true now rewrite N.eqb_eq, <- N.compare_eq_iff. Qed.

Lemma Neqb_complete n n' : N.eqb n n' = true -> n = n'.n, n':N
(n =? n') = true -> n = n'
Proof.n, n':N
(n =? n') = true -> n = n' now apply N.eqb_eq. Qed.

Lemma Nxor_eq_true n n' : N.lxor n n' = 0 -> N.eqb n n' = true.n, n':N
N.lxor n n' = 0 -> (n =? n') = true
Proof.n, n':N
N.lxor n n' = 0 -> (n =? n') = true
  intro H.n, n':N
H:N.lxor n n' = 0
(n =? n') = true apply N.lxor_eq in H.n, n':N
H:n = n'
(n =? n') = true subst.n':N
(n' =? n') = true apply N.eqb_refl.
Qed.

Ltac eqb2eq := rewrite <- ?not_true_iff_false in *; rewrite ?N.eqb_eq in *.

Lemma Nxor_eq_false n n' p :
  N.lxor n n' = N.pos p -> N.eqb n n' = false.n, n':N
p:positive
N.lxor n n' = N.pos p -> (n =? n') = false
Proof.n, n':N
p:positive
N.lxor n n' = N.pos p -> (n =? n') = false
  intros.n, n':N
p:positive
H:N.lxor n n' = N.pos p
(n =? n') = false eqb2eq.n, n':N
p:positive
H:N.lxor n n' = N.pos p
n <> n' intro.n, n':N
p:positive
H:N.lxor n n' = N.pos p
H0:n = n'
False subst.n':N
p:positive
H:N.lxor n' n' = N.pos p
False now rewrite N.lxor_nilpotent in *.
Qed.

Lemma Nodd_not_double a :
  Nodd a -> forall a0, N.eqb (N.double a0) a = false.a:N
Nodd a -> forall a0 : N, (N.double a0 =? a) = false
Proof.a:N
Nodd a -> forall a0 : N, (N.double a0 =? a) = false
  intros.a:N
H:Nodd a
a0:N
(N.double a0 =? a) = false eqb2eq.a:N
H:Nodd a
a0:N
N.double a0 <> a intros <-.a0:N
H:Nodd (N.double a0)
False
  unfold Nodd in *.a0:N
H:N.odd (N.double a0) = true
False now rewrite Ndouble_bit0 in *.
Qed.

Lemma Nnot_div2_not_double a a0 :
  N.eqb (N.div2 a) a0 = false -> N.eqb a (N.double a0) = false.a, a0:N
(N.div2 a =? a0) = false -> (a =? N.double a0) = false
Proof.a, a0:N
(N.div2 a =? a0) = false -> (a =? N.double a0) = false
  intros H.a, a0:N
H:(N.div2 a =? a0) = false
(a =? N.double a0) = false eqb2eq.a, a0:N
H:N.div2 a <> a0
a <> N.double a0 contradict H.a, a0:N
H:a = N.double a0
N.div2 a = a0 subst.a0:N
N.div2 (N.double a0) = a0 apply N.div2_double.
Qed.

Lemma Neven_not_double_plus_one a :
  Neven a -> forall a0, N.eqb (N.succ_double a0) a = false.a:N
Neven a ->
forall a0 : N, (N.succ_double a0 =? a) = false
Proof.a:N
Neven a ->
forall a0 : N, (N.succ_double a0 =? a) = false
  intros.a:N
H:Neven a
a0:N
(N.succ_double a0 =? a) = false eqb2eq.a:N
H:Neven a
a0:N
N.succ_double a0 <> a intros <-.a0:N
H:Neven (N.succ_double a0)
False
  unfold Neven in *.a0:N
H:N.odd (N.succ_double a0) = false
False now rewrite Ndouble_plus_one_bit0 in *.
Qed.

Lemma Nnot_div2_not_double_plus_one a a0 :
  N.eqb (N.div2 a) a0 = false -> N.eqb (N.succ_double a0) a = false.a, a0:N
(N.div2 a =? a0) = false ->
(N.succ_double a0 =? a) = false
Proof.a, a0:N
(N.div2 a =? a0) = false ->
(N.succ_double a0 =? a) = false
  intros H.a, a0:N
H:(N.div2 a =? a0) = false
(N.succ_double a0 =? a) = false eqb2eq.a, a0:N
H:N.div2 a <> a0
N.succ_double a0 <> a contradict H.a, a0:N
H:N.succ_double a0 = a
N.div2 a = a0 subst.a0:N
N.div2 (N.succ_double a0) = a0 apply N.div2_succ_double.
Qed.

Lemma Nbit0_neq a a' :
  N.odd a = false -> N.odd a' = true -> N.eqb a a' = false.a, a':N
N.odd a = false ->
N.odd a' = true -> (a =? a') = false
Proof.a, a':N
N.odd a = false ->
N.odd a' = true -> (a =? a') = false
  intros.a, a':N
H:N.odd a = false
H0:N.odd a' = true
(a =? a') = false eqb2eq.a, a':N
H:N.odd a <> true
H0:N.odd a' = true
a <> a' now intros <-.
Qed.

Lemma Ndiv2_eq a a' :
  N.eqb a a' = true -> N.eqb (N.div2 a) (N.div2 a') = true.a, a':N
(a =? a') = true -> (N.div2 a =? N.div2 a') = true
Proof.a, a':N
(a =? a') = true -> (N.div2 a =? N.div2 a') = true
  intros.a, a':N
H:(a =? a') = true
(N.div2 a =? N.div2 a') = true eqb2eq.a, a':N
H:a = a'
N.div2 a = N.div2 a' now subst.
Qed.

Lemma Ndiv2_neq a a' :
  N.eqb (N.div2 a) (N.div2 a') = false -> N.eqb a a' = false.a, a':N
(N.div2 a =? N.div2 a') = false -> (a =? a') = false
Proof.a, a':N
(N.div2 a =? N.div2 a') = false -> (a =? a') = false
  intros H.a, a':N
H:(N.div2 a =? N.div2 a') = false
(a =? a') = false eqb2eq.a, a':N
H:N.div2 a <> N.div2 a'
a <> a' contradict H.a, a':N
H:a = a'
N.div2 a = N.div2 a' now subst.
Qed.

Lemma Ndiv2_bit_eq a a' :
  N.odd a = N.odd a' -> N.div2 a = N.div2 a' -> a = a'.a, a':N
N.odd a = N.odd a' -> N.div2 a = N.div2 a' -> a = a'
Proof.a, a':N
N.odd a = N.odd a' -> N.div2 a = N.div2 a' -> a = a'
  intros H H'; now rewrite (N.div2_odd a), (N.div2_odd a'), H, H'.
Qed.

Lemma Ndiv2_bit_neq a a' :
  N.eqb a a' = false ->
   N.odd a = N.odd a' -> N.eqb (N.div2 a) (N.div2 a') = false.a, a':N
(a =? a') = false ->
N.odd a = N.odd a' -> (N.div2 a =? N.div2 a') = false
Proof.a, a':N
(a =? a') = false ->
N.odd a = N.odd a' -> (N.div2 a =? N.div2 a') = false
  intros H H'.a, a':N
H:(a =? a') = false
H':N.odd a = N.odd a'
(N.div2 a =? N.div2 a') = false eqb2eq.a, a':N
H:a <> a'
H':N.odd a = N.odd a'
N.div2 a <> N.div2 a' contradict H.a, a':N
H':N.odd a = N.odd a'
H:N.div2 a = N.div2 a'
a = a' now apply Ndiv2_bit_eq.
Qed.

Lemma Nneq_elim a a' :
   N.eqb a a' = false ->
   N.odd a = negb (N.odd a') \/
   N.eqb (N.div2 a) (N.div2 a') = false.a, a':N
(a =? a') = false ->
N.odd a = negb (N.odd a') \/
(N.div2 a =? N.div2 a') = false
Proof.a, a':N
(a =? a') = false ->
N.odd a = negb (N.odd a') \/
(N.div2 a =? N.div2 a') = false
  intros.a, a':N
H:(a =? a') = false
N.odd a = negb (N.odd a') \/
(N.div2 a =? N.div2 a') = false
  enough (N.odd a = N.odd a' \/ N.odd a = negb (N.odd a')) as [].a, a':N
H:(a =? a') = false
H0:N.odd a = N.odd a'
N.odd a = negb (N.odd a') \/
(N.div2 a =? N.div2 a') = false
a, a':N
H:(a =? a') = false
H0:N.odd a = negb (N.odd a')
N.odd a = negb (N.odd a') \/
(N.div2 a =? N.div2 a') = false
a, a':N
H:(a =? a') = false
N.odd a = N.odd a' \/ N.odd a = negb (N.odd a')
  -a, a':N
H:(a =? a') = false
H0:N.odd a = N.odd a'
N.odd a = negb (N.odd a') \/
(N.div2 a =? N.div2 a') = false right.a, a':N
H:(a =? a') = false
H0:N.odd a = N.odd a'
(N.div2 a =? N.div2 a') = false apply Ndiv2_bit_neq; assumption.
  -a, a':N
H:(a =? a') = false
H0:N.odd a = negb (N.odd a')
N.odd a = negb (N.odd a') \/
(N.div2 a =? N.div2 a') = false left.a, a':N
H:(a =? a') = false
H0:N.odd a = negb (N.odd a')
N.odd a = negb (N.odd a') assumption.
  -a, a':N
H:(a =? a') = false
N.odd a = N.odd a' \/ N.odd a = negb (N.odd a') case (N.odd a), (N.odd a'); auto.
Qed.

Lemma Ndouble_or_double_plus_un a :
   {a0 : N | a = N.double a0} + {a1 : N | a = N.succ_double a1}.a:N
({a0 : N | a = N.double a0} +
 {a1 : N | a = N.succ_double a1})%type
Proof.a:N
({a0 : N | a = N.double a0} +
 {a1 : N | a = N.succ_double a1})%type
  elim (sumbool_of_bool (N.odd a)); intros H; [right|left];
    exists (N.div2 a); symmetry;
    apply Ndiv2_double_plus_one || apply Ndiv2_double; auto.
Qed.

An inefficient boolean order on N. Please use N.leb instead now.

Definition Nleb (a b:N) := leb (N.to_nat a) (N.to_nat b).

Lemma Nleb_alt a b : Nleb a b = N.leb a b.a, b:N
Nleb a b = (a <=? b)
Proof.a, b:N
Nleb a b = (a <=? b)
 unfold Nleb.a, b:N
(N.to_nat a <=? N.to_nat b)%nat = (a <=? b)
 now rewrite eq_iff_eq_true, N.leb_le, leb_compare, <- N2Nat.inj_compare.
Qed.

Lemma Nleb_Nle a b : Nleb a b = true <-> a <= b.a, b:N
Nleb a b = true <-> a <= b
Proof.a, b:N
Nleb a b = true <-> a <= b now rewrite Nleb_alt, N.leb_le. Qed.

Lemma Nleb_refl a : Nleb a a = true.a:N
Nleb a a = true
Proof.a:N
Nleb a a = true rewrite Nleb_Nle; apply N.le_refl. Qed.

Lemma Nleb_antisym a b : Nleb a b = true -> Nleb b a = true -> a = b.a, b:N
Nleb a b = true -> Nleb b a = true -> a = b
Proof.a, b:N
Nleb a b = true -> Nleb b a = true -> a = b rewrite !Nleb_Nle.a, b:N
a <= b -> b <= a -> a = b apply N.le_antisymm. Qed.

Lemma Nleb_trans a b c : Nleb a b = true -> Nleb b c = true -> Nleb a c = true.a, b, c:N
Nleb a b = true -> Nleb b c = true -> Nleb a c = true
Proof.a, b, c:N
Nleb a b = true -> Nleb b c = true -> Nleb a c = true rewrite !Nleb_Nle.a, b, c:N
a <= b -> b <= c -> a <= c apply N.le_trans. Qed.

Lemma Nleb_ltb_trans a b c :
  Nleb a b = true -> Nleb c b = false -> Nleb c a = false.a, b, c:N
Nleb a b = true ->
Nleb c b = false -> Nleb c a = false
Proof.a, b, c:N
Nleb a b = true ->
Nleb c b = false -> Nleb c a = false
  unfold Nleb.a, b, c:N
(N.to_nat a <=? N.to_nat b)%nat = true ->
(N.to_nat c <=? N.to_nat b)%nat = false ->
(N.to_nat c <=? N.to_nat a)%nat = false intros.a, b, c:N
H:(N.to_nat a <=? N.to_nat b)%nat = true
H0:(N.to_nat c <=? N.to_nat b)%nat = false
(N.to_nat c <=? N.to_nat a)%nat = false apply leb_correct_conv.a, b, c:N
H:(N.to_nat a <=? N.to_nat b)%nat = true
H0:(N.to_nat c <=? N.to_nat b)%nat = false
(N.to_nat a < N.to_nat c)%nat
  apply le_lt_trans with (m := N.to_nat b).a, b, c:N
H:(N.to_nat a <=? N.to_nat b)%nat = true
H0:(N.to_nat c <=? N.to_nat b)%nat = false
(N.to_nat a <= N.to_nat b)%nat
a, b, c:N
H:(N.to_nat a <=? N.to_nat b)%nat = true
H0:(N.to_nat c <=? N.to_nat b)%nat = false
(N.to_nat b < N.to_nat c)%nat
  apply leb_complete.a, b, c:N
H:(N.to_nat a <=? N.to_nat b)%nat = true
H0:(N.to_nat c <=? N.to_nat b)%nat = false
(N.to_nat a <=? N.to_nat b)%nat = true
a, b, c:N
H:(N.to_nat a <=? N.to_nat b)%nat = true
H0:(N.to_nat c <=? N.to_nat b)%nat = false
(N.to_nat b < N.to_nat c)%nat assumption.a, b, c:N
H:(N.to_nat a <=? N.to_nat b)%nat = true
H0:(N.to_nat c <=? N.to_nat b)%nat = false
(N.to_nat b < N.to_nat c)%nat
  apply leb_complete_conv.a, b, c:N
H:(N.to_nat a <=? N.to_nat b)%nat = true
H0:(N.to_nat c <=? N.to_nat b)%nat = false
(N.to_nat c <=? N.to_nat b)%nat = false assumption.
Qed.

Lemma Nltb_leb_trans a b c :
  Nleb b a = false -> Nleb b c = true -> Nleb c a = false.a, b, c:N
Nleb b a = false ->
Nleb b c = true -> Nleb c a = false
Proof.a, b, c:N
Nleb b a = false ->
Nleb b c = true -> Nleb c a = false
  unfold Nleb.a, b, c:N
(N.to_nat b <=? N.to_nat a)%nat = false ->
(N.to_nat b <=? N.to_nat c)%nat = true ->
(N.to_nat c <=? N.to_nat a)%nat = false intros.a, b, c:N
H:(N.to_nat b <=? N.to_nat a)%nat = false
H0:(N.to_nat b <=? N.to_nat c)%nat = true
(N.to_nat c <=? N.to_nat a)%nat = false apply leb_correct_conv.a, b, c:N
H:(N.to_nat b <=? N.to_nat a)%nat = false
H0:(N.to_nat b <=? N.to_nat c)%nat = true
(N.to_nat a < N.to_nat c)%nat
  apply lt_le_trans with (m := N.to_nat b).a, b, c:N
H:(N.to_nat b <=? N.to_nat a)%nat = false
H0:(N.to_nat b <=? N.to_nat c)%nat = true
(N.to_nat a < N.to_nat b)%nat
a, b, c:N
H:(N.to_nat b <=? N.to_nat a)%nat = false
H0:(N.to_nat b <=? N.to_nat c)%nat = true
(N.to_nat b <= N.to_nat c)%nat
  apply leb_complete_conv.a, b, c:N
H:(N.to_nat b <=? N.to_nat a)%nat = false
H0:(N.to_nat b <=? N.to_nat c)%nat = true
(N.to_nat b <=? N.to_nat a)%nat = false
a, b, c:N
H:(N.to_nat b <=? N.to_nat a)%nat = false
H0:(N.to_nat b <=? N.to_nat c)%nat = true
(N.to_nat b <= N.to_nat c)%nat assumption.a, b, c:N
H:(N.to_nat b <=? N.to_nat a)%nat = false
H0:(N.to_nat b <=? N.to_nat c)%nat = true
(N.to_nat b <= N.to_nat c)%nat
  apply leb_complete.a, b, c:N
H:(N.to_nat b <=? N.to_nat a)%nat = false
H0:(N.to_nat b <=? N.to_nat c)%nat = true
(N.to_nat b <=? N.to_nat c)%nat = true assumption.
Qed.

Lemma Nltb_trans a b c :
  Nleb b a = false -> Nleb c b = false -> Nleb c a = false.a, b, c:N
Nleb b a = false ->
Nleb c b = false -> Nleb c a = false
Proof.a, b, c:N
Nleb b a = false ->
Nleb c b = false -> Nleb c a = false
  unfold Nleb.a, b, c:N
(N.to_nat b <=? N.to_nat a)%nat = false ->
(N.to_nat c <=? N.to_nat b)%nat = false ->
(N.to_nat c <=? N.to_nat a)%nat = false intros.a, b, c:N
H:(N.to_nat b <=? N.to_nat a)%nat = false
H0:(N.to_nat c <=? N.to_nat b)%nat = false
(N.to_nat c <=? N.to_nat a)%nat = false apply leb_correct_conv.a, b, c:N
H:(N.to_nat b <=? N.to_nat a)%nat = false
H0:(N.to_nat c <=? N.to_nat b)%nat = false
(N.to_nat a < N.to_nat c)%nat
  apply lt_trans with (m := N.to_nat b).a, b, c:N
H:(N.to_nat b <=? N.to_nat a)%nat = false
H0:(N.to_nat c <=? N.to_nat b)%nat = false
(N.to_nat a < N.to_nat b)%nat
a, b, c:N
H:(N.to_nat b <=? N.to_nat a)%nat = false
H0:(N.to_nat c <=? N.to_nat b)%nat = false
(N.to_nat b < N.to_nat c)%nat
  apply leb_complete_conv.a, b, c:N
H:(N.to_nat b <=? N.to_nat a)%nat = false
H0:(N.to_nat c <=? N.to_nat b)%nat = false
(N.to_nat b <=? N.to_nat a)%nat = false
a, b, c:N
H:(N.to_nat b <=? N.to_nat a)%nat = false
H0:(N.to_nat c <=? N.to_nat b)%nat = false
(N.to_nat b < N.to_nat c)%nat assumption.a, b, c:N
H:(N.to_nat b <=? N.to_nat a)%nat = false
H0:(N.to_nat c <=? N.to_nat b)%nat = false
(N.to_nat b < N.to_nat c)%nat
  apply leb_complete_conv.a, b, c:N
H:(N.to_nat b <=? N.to_nat a)%nat = false
H0:(N.to_nat c <=? N.to_nat b)%nat = false
(N.to_nat c <=? N.to_nat b)%nat = false assumption.
Qed.

Lemma Nltb_leb_weak a b : Nleb b a = false -> Nleb a b = true.a, b:N
Nleb b a = false -> Nleb a b = true
Proof.a, b:N
Nleb b a = false -> Nleb a b = true
  unfold Nleb.a, b:N
(N.to_nat b <=? N.to_nat a)%nat = false ->
(N.to_nat a <=? N.to_nat b)%nat = true intros.a, b:N
H:(N.to_nat b <=? N.to_nat a)%nat = false
(N.to_nat a <=? N.to_nat b)%nat = true apply leb_correct.a, b:N
H:(N.to_nat b <=? N.to_nat a)%nat = false
(N.to_nat a <= N.to_nat b)%nat apply lt_le_weak.a, b:N
H:(N.to_nat b <=? N.to_nat a)%nat = false
(N.to_nat a < N.to_nat b)%nat
  apply leb_complete_conv.a, b:N
H:(N.to_nat b <=? N.to_nat a)%nat = false
(N.to_nat b <=? N.to_nat a)%nat = false assumption.
Qed.

Lemma Nleb_double_mono a b :
  Nleb a b = true -> Nleb (N.double a) (N.double b) = true.a, b:N
Nleb a b = true ->
Nleb (N.double a) (N.double b) = true
Proof.a, b:N
Nleb a b = true ->
Nleb (N.double a) (N.double b) = true
  unfold Nleb.a, b:N
(N.to_nat a <=? N.to_nat b)%nat = true ->
(N.to_nat (N.double a) <=? N.to_nat (N.double b))%nat =
true intros.a, b:N
H:(N.to_nat a <=? N.to_nat b)%nat = true
(N.to_nat (N.double a) <=? N.to_nat (N.double b))%nat =
true rewrite !N2Nat.inj_double.a, b:N
H:(N.to_nat a <=? N.to_nat b)%nat = true
(2 * N.to_nat a <=? 2 * N.to_nat b)%nat = true apply leb_correct.a, b:N
H:(N.to_nat a <=? N.to_nat b)%nat = true
(2 * N.to_nat a <= 2 * N.to_nat b)%nat
  apply mult_le_compat_l.a, b:N
H:(N.to_nat a <=? N.to_nat b)%nat = true
(N.to_nat a <= N.to_nat b)%nat now apply leb_complete.
Qed.

Lemma Nleb_double_plus_one_mono a b :
  Nleb a b = true ->
   Nleb (N.succ_double a) (N.succ_double b) = true.a, b:N
Nleb a b = true ->
Nleb (N.succ_double a) (N.succ_double b) = true
Proof.a, b:N
Nleb a b = true ->
Nleb (N.succ_double a) (N.succ_double b) = true
  unfold Nleb.a, b:N
(N.to_nat a <=? N.to_nat b)%nat = true ->
(N.to_nat (N.succ_double a) <=?
 N.to_nat (N.succ_double b))%nat = true intros.a, b:N
H:(N.to_nat a <=? N.to_nat b)%nat = true
(N.to_nat (N.succ_double a) <=?
 N.to_nat (N.succ_double b))%nat = true rewrite !N2Nat.inj_succ_double.a, b:N
H:(N.to_nat a <=? N.to_nat b)%nat = true
(S (2 * N.to_nat a) <=? S (2 * N.to_nat b))%nat = true apply leb_correct.a, b:N
H:(N.to_nat a <=? N.to_nat b)%nat = true
(S (2 * N.to_nat a) <= S (2 * N.to_nat b))%nat
  apply le_n_S, mult_le_compat_l.a, b:N
H:(N.to_nat a <=? N.to_nat b)%nat = true
(N.to_nat a <= N.to_nat b)%nat now apply leb_complete.
Qed.

Lemma Nleb_double_mono_conv a b :
  Nleb (N.double a) (N.double b) = true -> Nleb a b = true.a, b:N
Nleb (N.double a) (N.double b) = true ->
Nleb a b = true
Proof.a, b:N
Nleb (N.double a) (N.double b) = true ->
Nleb a b = true
  unfold Nleb.a, b:N
(N.to_nat (N.double a) <=? N.to_nat (N.double b))%nat =
true -> (N.to_nat a <=? N.to_nat b)%nat = true rewrite !N2Nat.inj_double.a, b:N
(2 * N.to_nat a <=? 2 * N.to_nat b)%nat = true ->
(N.to_nat a <=? N.to_nat b)%nat = true intro.a, b:N
H:(2 * N.to_nat a <=? 2 * N.to_nat b)%nat = true
(N.to_nat a <=? N.to_nat b)%nat = true apply leb_correct.a, b:N
H:(2 * N.to_nat a <=? 2 * N.to_nat b)%nat = true
(N.to_nat a <= N.to_nat b)%nat
  apply (mult_S_le_reg_l 1).a, b:N
H:(2 * N.to_nat a <=? 2 * N.to_nat b)%nat = true
(2 * N.to_nat a <= 2 * N.to_nat b)%nat now apply leb_complete.
Qed.

Lemma Nleb_double_plus_one_mono_conv a b :
  Nleb (N.succ_double a) (N.succ_double b) = true ->
   Nleb a b = true.a, b:N
Nleb (N.succ_double a) (N.succ_double b) = true ->
Nleb a b = true
Proof.a, b:N
Nleb (N.succ_double a) (N.succ_double b) = true ->
Nleb a b = true
  unfold Nleb.a, b:N
(N.to_nat (N.succ_double a) <=?
 N.to_nat (N.succ_double b))%nat = true ->
(N.to_nat a <=? N.to_nat b)%nat = true rewrite !N2Nat.inj_succ_double.a, b:N
(S (2 * N.to_nat a) <=? S (2 * N.to_nat b))%nat = true ->
(N.to_nat a <=? N.to_nat b)%nat = true intro.a, b:N
H:(S (2 * N.to_nat a) <=? S (2 * N.to_nat b))%nat =
true
(N.to_nat a <=? N.to_nat b)%nat = true apply leb_correct.a, b:N
H:(S (2 * N.to_nat a) <=? S (2 * N.to_nat b))%nat =
true
(N.to_nat a <= N.to_nat b)%nat
  apply (mult_S_le_reg_l 1).a, b:N
H:(S (2 * N.to_nat a) <=? S (2 * N.to_nat b))%nat =
true
(2 * N.to_nat a <= 2 * N.to_nat b)%nat apply le_S_n.a, b:N
H:(S (2 * N.to_nat a) <=? S (2 * N.to_nat b))%nat =
true
(S (2 * N.to_nat a) <= S (2 * N.to_nat b))%nat now apply leb_complete.
Qed.

Lemma Nltb_double_mono a b :
   Nleb a b = false -> Nleb (N.double a) (N.double b) = false.a, b:N
Nleb a b = false ->
Nleb (N.double a) (N.double b) = false
Proof.a, b:N
Nleb a b = false ->
Nleb (N.double a) (N.double b) = false
  intros.a, b:N
H:Nleb a b = false
Nleb (N.double a) (N.double b) = false elim (sumbool_of_bool (Nleb (N.double a) (N.double b))).a, b:N
H:Nleb a b = false
Nleb (N.double a) (N.double b) = true ->
Nleb (N.double a) (N.double b) = false
a, b:N
H:Nleb a b = false
Nleb (N.double a) (N.double b) = false ->
Nleb (N.double a) (N.double b) = false intro H0.a, b:N
H:Nleb a b = false
H0:Nleb (N.double a) (N.double b) = true
Nleb (N.double a) (N.double b) = false
a, b:N
H:Nleb a b = false
Nleb (N.double a) (N.double b) = false ->
Nleb (N.double a) (N.double b) = false
  rewrite (Nleb_double_mono_conv _ _ H0) in H.a, b:N
H:true = false
H0:Nleb (N.double a) (N.double b) = true
Nleb (N.double a) (N.double b) = false
a, b:N
H:Nleb a b = false
Nleb (N.double a) (N.double b) = false ->
Nleb (N.double a) (N.double b) = false discriminate H.a, b:N
H:Nleb a b = false
Nleb (N.double a) (N.double b) = false ->
Nleb (N.double a) (N.double b) = false
  trivial.
Qed.

Lemma Nltb_double_plus_one_mono a b :
  Nleb a b = false ->
   Nleb (N.succ_double a) (N.succ_double b) = false.a, b:N
Nleb a b = false ->
Nleb (N.succ_double a) (N.succ_double b) = false
Proof.a, b:N
Nleb a b = false ->
Nleb (N.succ_double a) (N.succ_double b) = false
  intros.a, b:N
H:Nleb a b = false
Nleb (N.succ_double a) (N.succ_double b) = false elim (sumbool_of_bool (Nleb (N.succ_double a) (N.succ_double b))).a, b:N
H:Nleb a b = false
Nleb (N.succ_double a) (N.succ_double b) = true ->
Nleb (N.succ_double a) (N.succ_double b) = false
a, b:N
H:Nleb a b = false
Nleb (N.succ_double a) (N.succ_double b) = false ->
Nleb (N.succ_double a) (N.succ_double b) = false
  intro H0.a, b:N
H:Nleb a b = false
H0:Nleb (N.succ_double a) (N.succ_double b) = true
Nleb (N.succ_double a) (N.succ_double b) = false
a, b:N
H:Nleb a b = false
Nleb (N.succ_double a) (N.succ_double b) = false ->
Nleb (N.succ_double a) (N.succ_double b) = false
  rewrite (Nleb_double_plus_one_mono_conv _ _ H0) in H.a, b:N
H:true = false
H0:Nleb (N.succ_double a) (N.succ_double b) = true
Nleb (N.succ_double a) (N.succ_double b) = false
a, b:N
H:Nleb a b = false
Nleb (N.succ_double a) (N.succ_double b) = false ->
Nleb (N.succ_double a) (N.succ_double b) = false discriminate H.a, b:N
H:Nleb a b = false
Nleb (N.succ_double a) (N.succ_double b) = false ->
Nleb (N.succ_double a) (N.succ_double b) = false
  trivial.
Qed.

Lemma Nltb_double_mono_conv a b :
  Nleb (N.double a) (N.double b) = false -> Nleb a b = false.a, b:N
Nleb (N.double a) (N.double b) = false ->
Nleb a b = false
Proof.a, b:N
Nleb (N.double a) (N.double b) = false ->
Nleb a b = false
  intros.a, b:N
H:Nleb (N.double a) (N.double b) = false
Nleb a b = false elim (sumbool_of_bool (Nleb a b)).a, b:N
H:Nleb (N.double a) (N.double b) = false
Nleb a b = true -> Nleb a b = false
a, b:N
H:Nleb (N.double a) (N.double b) = false
Nleb a b = false -> Nleb a b = false intro H0.a, b:N
H:Nleb (N.double a) (N.double b) = false
H0:Nleb a b = true
Nleb a b = false
a, b:N
H:Nleb (N.double a) (N.double b) = false
Nleb a b = false -> Nleb a b = false
  rewrite (Nleb_double_mono _ _ H0) in H.a, b:N
H:true = false
H0:Nleb a b = true
Nleb a b = false
a, b:N
H:Nleb (N.double a) (N.double b) = false
Nleb a b = false -> Nleb a b = false discriminate H.a, b:N
H:Nleb (N.double a) (N.double b) = false
Nleb a b = false -> Nleb a b = false
  trivial.
Qed.

Lemma Nltb_double_plus_one_mono_conv a b :
  Nleb (N.succ_double a) (N.succ_double b) = false ->
   Nleb a b = false.a, b:N
Nleb (N.succ_double a) (N.succ_double b) = false ->
Nleb a b = false
Proof.a, b:N
Nleb (N.succ_double a) (N.succ_double b) = false ->
Nleb a b = false
  intros.a, b:N
H:Nleb (N.succ_double a) (N.succ_double b) = false
Nleb a b = false elim (sumbool_of_bool (Nleb a b)).a, b:N
H:Nleb (N.succ_double a) (N.succ_double b) = false
Nleb a b = true -> Nleb a b = false
a, b:N
H:Nleb (N.succ_double a) (N.succ_double b) = false
Nleb a b = false -> Nleb a b = false intro H0.a, b:N
H:Nleb (N.succ_double a) (N.succ_double b) = false
H0:Nleb a b = true
Nleb a b = false
a, b:N
H:Nleb (N.succ_double a) (N.succ_double b) = false
Nleb a b = false -> Nleb a b = false
  rewrite (Nleb_double_plus_one_mono _ _ H0) in H.a, b:N
H:true = false
H0:Nleb a b = true
Nleb a b = false
a, b:N
H:Nleb (N.succ_double a) (N.succ_double b) = false
Nleb a b = false -> Nleb a b = false discriminate H.a, b:N
H:Nleb (N.succ_double a) (N.succ_double b) = false
Nleb a b = false -> Nleb a b = false
  trivial.
Qed.

(* Nleb and N.compare *)

(* NB: No need to prove that Nleb a b = true <-> N.compare a b <> Gt,
   this statement is in fact Nleb_Nle! *)

Lemma Nltb_Ncompare a b : Nleb a b = false <-> N.compare a b = Gt.a, b:N
Nleb a b = false <-> (a ?= b) = Gt
Proof.a, b:N
Nleb a b = false <-> (a ?= b) = Gt
  now rewrite N.compare_nle_iff, <- Nleb_Nle, not_true_iff_false.
Qed.

Lemma Ncompare_Gt_Nltb a b : N.compare a b = Gt -> Nleb a b = false.a, b:N
(a ?= b) = Gt -> Nleb a b = false
Proof.a, b:N
(a ?= b) = Gt -> Nleb a b = false apply <- Nltb_Ncompare; auto. Qed.

Lemma Ncompare_Lt_Nltb a b : N.compare a b = Lt -> Nleb b a = false.a, b:N
(a ?= b) = Lt -> Nleb b a = false
Proof.a, b:N
(a ?= b) = Lt -> Nleb b a = false
 intros H.a, b:N
H:(a ?= b) = Lt
Nleb b a = false rewrite Nltb_Ncompare, N.compare_antisym, H; auto.
Qed.

(* Old results about [N.min] *)

Notation Nmin_choice := N.min_dec (only parsing).

Lemma Nmin_le_1 a b : Nleb (N.min a b) a = true.a, b:N
Nleb (N.min a b) a = true
Proof.a, b:N
Nleb (N.min a b) a = true rewrite Nleb_Nle.a, b:N
N.min a b <= a apply N.le_min_l. Qed.

Lemma Nmin_le_2 a b : Nleb (N.min a b) b = true.a, b:N
Nleb (N.min a b) b = true
Proof.a, b:N
Nleb (N.min a b) b = true rewrite Nleb_Nle.a, b:N
N.min a b <= b apply N.le_min_r. Qed.

Lemma Nmin_le_3 a b c : Nleb a (N.min b c) = true -> Nleb a b = true.a, b, c:N
Nleb a (N.min b c) = true -> Nleb a b = true
Proof.a, b, c:N
Nleb a (N.min b c) = true -> Nleb a b = true rewrite !Nleb_Nle.a, b, c:N
a <= N.min b c -> a <= b apply N.min_glb_l. Qed.

Lemma Nmin_le_4 a b c : Nleb a (N.min b c) = true -> Nleb a c = true.a, b, c:N
Nleb a (N.min b c) = true -> Nleb a c = true
Proof.a, b, c:N
Nleb a (N.min b c) = true -> Nleb a c = true rewrite !Nleb_Nle.a, b, c:N
a <= N.min b c -> a <= c apply N.min_glb_r. Qed.

Lemma Nmin_le_5 a b c :
   Nleb a b = true -> Nleb a c = true -> Nleb a (N.min b c) = true.a, b, c:N
Nleb a b = true ->
Nleb a c = true -> Nleb a (N.min b c) = true
Proof.a, b, c:N
Nleb a b = true ->
Nleb a c = true -> Nleb a (N.min b c) = true rewrite !Nleb_Nle.a, b, c:N
a <= b -> a <= c -> a <= N.min b c apply N.min_glb. Qed.

Lemma Nmin_lt_3 a b c : Nleb (N.min b c) a = false -> Nleb b a = false.a, b, c:N
Nleb (N.min b c) a = false -> Nleb b a = false
Proof.a, b, c:N
Nleb (N.min b c) a = false -> Nleb b a = false
  rewrite <- !not_true_iff_false, !Nleb_Nle.a, b, c:N
~ N.min b c <= a -> ~ b <= a
  rewrite N.min_le_iff; auto.
Qed.

Lemma Nmin_lt_4 a b c : Nleb (N.min b c) a = false -> Nleb c a = false.a, b, c:N
Nleb (N.min b c) a = false -> Nleb c a = false
Proof.a, b, c:N
Nleb (N.min b c) a = false -> Nleb c a = false
  rewrite <- !not_true_iff_false, !Nleb_Nle.a, b, c:N
~ N.min b c <= a -> ~ c <= a
  rewrite N.min_le_iff; auto.
Qed.