Library additions.Dichotomy

From Coq Require Import Arith NArith.
From additions Require Export Strategies Pow Compatibility
  More_on_positive.

Open Scope positive_scope.

Function dicho_aux (p:positive) {struct p} : positive :=
 match p with
   | 1%positive ⇒ xH
   | 2%positive | 3%positive ⇒ 2
   | xO (xO q) | xO (xI q) | xI (xO q) | xI (xI q) ⇒
                                         xO (dicho_aux q)
 end.

Definition dicho (p:positive) : positive :=
  N2pos (N.div (Npos p) (Npos (dicho_aux p))).

Lemma dicho_aux_xOxO : ∀ p: positive,
                          dicho_aux (xO (xO p)) = xO (dicho_aux p).

Lemma dicho_aux_xOxI : ∀ p: positive,
                          dicho_aux (xO (xI p)) = xO (dicho_aux p).

Lemma dicho_aux_xIxO : ∀ p: positive,
                          dicho_aux (xI (xO p)) = xO (dicho_aux p).

Lemma dicho_aux_xIxI : ∀ p: positive,
                          dicho_aux (xI (xI p)) = xO (dicho_aux p).

Lemma dicho_aux_le_xOXO :
  ∀ p:positive , xO (dicho_aux p) ≤ p →
                       xO (dicho_aux (p~0~0)) ≤ p~0~0.

Lemma dicho_aux_le_xOXI :
  ∀ p:positive , xO (dicho_aux p) ≤ p →
                      xO (dicho_aux (p~0~1)) ≤ p~0~1.

Lemma dicho_aux_le_xIXO :
  ∀ p:positive , xO (dicho_aux p) ≤ p →
                      xO (dicho_aux (p~1~0)) ≤ p~1~0.

Lemma dicho_aux_le_xIXI :
  ∀ p:positive , xO (dicho_aux p) ≤ p →
                      xO (dicho_aux (p~1~1)) ≤ p~1~1.

#[global] Hint Resolve dicho_aux_le_xOXO dicho_aux_le_xOXI
             dicho_aux_le_xIXO dicho_aux_le_xIXI : chains.

Lemma dicho_aux_lt : ∀ p, 3 < p →
                               xO (dicho_aux p) ≤ p.

Lemma dicho_aux_gt : ∀ p, 3 < p → 1 < dicho_aux p.

Lemma dicho_lt : ∀ p:positive, 3 < p → dicho p < p.

Lemma dicho_gt : ∀ p:positive, 3 < p → 1 < dicho p.

#[ global ] Instance Dicho_strat : Strategy dicho.