Require Export BinNums.
Require Import Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid
 Equalities Orders OrdersFacts GenericMinMax Le Plus.

Require Export BinPosDef.

Local Open Scope positive_scope.
LocalLocal

Module Pos
 <: UsualOrderedTypeFull
 <: UsualDecidableTypeFull
 <: TotalOrder.

Include BinPosDef.Pos.

Definition eq := @Logic.eq positive.
Definition eq_equiv := @eq_equivalence positive.
Include BackportEq.

Definition lt x y := (x ?= y) = Lt.
Definition gt x y := (x ?= y) = Gt.
Definition le x y := (x ?= y) <> Gt.
Definition ge x y := (x ?= y) <> Lt.

Infix "<=" := le : positive_scope.
Infix "<" := lt : positive_scope.
Infix ">=" := ge : positive_scope.
Infix ">" := gt : positive_scope.

Notation "x <= y <= z" := (x <= y /\ y <= z) : positive_scope.
Notation "x <= y < z" := (x <= y /\ y < z) : positive_scope.
Notation "x < y < z" := (x < y /\ y < z) : positive_scope.
Notation "x < y <= z" := (x < y /\ y <= z) : positive_scope.

Lemma eq_dec : forall x y:positive, {x = y} + {x <> y}.

Lemma xI_succ_xO p : p~1 = succ p~0.

Lemma succ_discr p : p <> succ p.

Lemma pred_double_spec p : pred_double p = pred (p~0).

Lemma succ_pred_double p : succ (pred_double p) = p~0.

Lemma pred_double_succ p : pred_double (succ p) = p~1.

Lemma double_succ p : (succ p)~0 = succ (succ p~0).

Lemma pred_double_xO_discr p : pred_double p <> p~0.

Lemma succ_not_1 p : succ p <> 1.

Lemma pred_succ p : pred (succ p) = p.

Lemma succ_pred_or p : p = 1 \/ succ (pred p) = p.

Lemma succ_pred p : p <> 1 -> succ (pred p) = p.

Lemma succ_inj p q : succ p = succ q -> p = q.

Lemma pred_N_succ p : pred_N (succ p) = Npos p.

Lemma add_1_r p : p + 1 = succ p.

Lemma add_1_l p : 1 + p = succ p.

Theorem add_carry_spec p q : add_carry p q = succ (p + q).

Theorem add_comm p q : p + q = q + p.

Theorem add_succ_r p q : p + succ q = succ (p + q).

Theorem add_succ_l p q : succ p + q = succ (p + q).

Lemma add_no_neutral p q : q + p <> p.

Lemma add_carry_add p q r s :
  add_carry p r = add_carry q s -> p + r = q + s.

Lemma add_reg_r p q r : p + r = q + r -> p = q.

Lemma add_reg_l p q r : p + q = p + r -> q = r.

Lemma add_cancel_r p q r : p + r = q + r <-> p = q.

Lemma add_cancel_l p q r : r + p = r + q <-> p = q.

Lemma add_carry_reg_r p q r :
  add_carry p r = add_carry q r -> p = q.

Lemma add_carry_reg_l p q r :
  add_carry p q = add_carry p r -> q = r.

Theorem add_assoc p q r : p + (q + r) = p + q + r.

Lemma add_xO p q : (p + q)~0 = p~0 + q~0.

Lemma add_xI_pred_double p q :
  (p + q)~0 = p~1 + pred_double q.

Lemma add_xO_pred_double p q :
  pred_double (p + q) = p~0 + pred_double q.

Lemma add_diag p : p + p = p~0.

Fixpoint peano_rect (P:positive->Type) (a:P 1)
  (f: forall p:positive, P p -> P (succ p)) (p:positive) : P p :=
let f2 := peano_rect (fun p:positive => P (p~0)) (f _ a)
  (fun (p:positive) (x:P (p~0)) => f _ (f _ x))
in
match p with
  | q~1 => f _ (f2 q)
  | q~0 => f2 q
  | 1 => a
end.

Theorem peano_rect_succ (P:positive->Type) (a:P 1)
  (f:forall p, P p -> P (succ p)) (p:positive) :
  peano_rect P a f (succ p) = f _ (peano_rect P a f p).

Theorem peano_rect_base (P:positive->Type) (a:P 1)
  (f:forall p, P p -> P (succ p)) :
  peano_rect P a f 1 = a.

Definition peano_rec (P:positive->Set) := peano_rect P.

Definition peano_ind (P:positive->Prop) := peano_rect P.

Theorem peano_case :
  forall P:positive -> Prop,
    P 1 -> (forall n:positive, P (succ n)) -> forall p:positive, P p.

Inductive PeanoView : positive -> Type :=
| PeanoOne : PeanoView 1
| PeanoSucc : forall p, PeanoView p -> PeanoView (succ p).

Fixpoint peanoView_xO p (q:PeanoView p) : PeanoView (p~0) :=
  match q in PeanoView x return PeanoView (x~0) with
    | PeanoOne => PeanoSucc _ PeanoOne
    | PeanoSucc _ q => PeanoSucc _ (PeanoSucc _ (peanoView_xO _ q))
  end.

Fixpoint peanoView_xI p (q:PeanoView p) : PeanoView (p~1) :=
  match q in PeanoView x return PeanoView (x~1) with
    | PeanoOne => PeanoSucc _ (PeanoSucc _ PeanoOne)
    | PeanoSucc _ q => PeanoSucc _ (PeanoSucc _ (peanoView_xI _ q))
  end.

Fixpoint peanoView p : PeanoView p :=
  match p return PeanoView p with
    | 1 => PeanoOne
    | p~0 => peanoView_xO p (peanoView p)
    | p~1 => peanoView_xI p (peanoView p)
  end.

Definition PeanoView_iter (P:positive->Type)
  (a:P 1) (f:forall p, P p -> P (succ p)) :=
  (fix iter p (q:PeanoView p) : P p :=
    match q in PeanoView p return P p with
      | PeanoOne => a
      | PeanoSucc _ q => f _ (iter _ q)
    end).

Theorem eq_dep_eq_positive :
  forall (P:positive->Type) (p:positive) (x y:P p),
    eq_dep positive P p x p y -> x = y.

Theorem PeanoViewUnique : forall p (q q´:PeanoView p), q = q´.

Lemma peano_equiv (P:positive->Type) (a:P 1) (f:forall p, P p -> P (succ p)) p :
   PeanoView_iter P a f p (peanoView p) = peano_rect P a f p.

Lemma mul_1_l p : 1 * p = p.

Lemma mul_1_r p : p * 1 = p.

Lemma mul_xO_r p q : p * q~0 = (p * q)~0.

Lemma mul_xI_r p q : p * q~1 = p + (p * q)~0.

Theorem mul_comm p q : p * q = q * p.

Theorem mul_add_distr_l p q r :
  p * (q + r) = p * q + p * r.

Theorem mul_add_distr_r p q r :
  (p + q) * r = p * r + q * r.

Theorem mul_assoc p q r : p * (q * r) = p * q * r.

Lemma mul_succ_l p q : (succ p) * q = q + p * q.

Lemma mul_succ_r p q : p * (succ q) = p + p * q.

Lemma mul_xI_mul_xO_discr p q r : p~1 * r <> q~0 * r.

Lemma mul_xO_discr p q : p~0 * q <> q.

Theorem mul_reg_r p q r : p * r = q * r -> p = q.

Theorem mul_reg_l p q r : r * p = r * q -> p = q.

Lemma mul_cancel_r p q r : p * r = q * r <-> p = q.

Lemma mul_cancel_l p q r : r * p = r * q <-> p = q.

Lemma mul_eq_1_l p q : p * q = 1 -> p = 1.

Lemma mul_eq_1_r p q : p * q = 1 -> q = 1.

Notation mul_eq_1 := mul_eq_1_l.

Lemma square_xO p : p~0 * p~0 = (p*p)~0~0.

Lemma square_xI p : p~1 * p~1 = (p*p+p)~0~1.

Lemma iter_swap_gen : forall A B (f:A->B)(g:A->A)(h:B->B),
 (forall a, f (g a) = h (f a)) -> forall p a,
 f (iter p g a) = iter p h (f a).

Theorem iter_swap :
  forall p (A:Type) (f:A -> A) (x:A),
    iter p f (f x) = f (iter p f x).

Theorem iter_succ :
  forall p (A:Type) (f:A -> A) (x:A),
    iter (succ p) f x = f (iter p f x).

Theorem iter_add :
  forall p q (A:Type) (f:A -> A) (x:A),
    iter (p+q) f x = iter p f (iter q f x).

Theorem iter_invariant :
  forall (p:positive) (A:Type) (f:A -> A) (Inv:A -> Prop),
    (forall x:A, Inv x -> Inv (f x)) ->
    forall x:A, Inv x -> Inv (iter p f x).

Lemma pow_1_r p : p^1 = p.

Lemma pow_succ_r p q : p^(succ q) = p * p^q.

Lemma square_spec p : square p = p * p.

Lemma sub_mask_succ_r p q :
  sub_mask p (succ q) = sub_mask_carry p q.

Theorem sub_mask_carry_spec p q :
  sub_mask_carry p q = pred_mask (sub_mask p q).

Inductive SubMaskSpec (p q : positive) : mask -> Prop :=
 | SubIsNul : p = q -> SubMaskSpec p q IsNul
 | SubIsPos : forall r, q + r = p -> SubMaskSpec p q (IsPos r)
 | SubIsNeg : forall r, p + r = q -> SubMaskSpec p q IsNeg.

Theorem sub_mask_spec p q : SubMaskSpec p q (sub_mask p q).

Theorem sub_mask_nul_iff p q : sub_mask p q = IsNul <-> p = q.

Theorem sub_mask_diag p : sub_mask p p = IsNul.

Lemma sub_mask_add p q r : sub_mask p q = IsPos r -> q + r = p.

Lemma sub_mask_add_diag_l p q : sub_mask (p+q) p = IsPos q.

Lemma sub_mask_pos_iff p q r : sub_mask p q = IsPos r <-> q + r = p.

Lemma sub_mask_add_diag_r p q : sub_mask p (p+q) = IsNeg.

Lemma sub_mask_neg_iff p q : sub_mask p q = IsNeg <-> exists r, p + r = q.

Theorem eqb_eq p q : (p =? q) = true <-> p=q.

Theorem ltb_lt p q : (p <? q) = true <-> p < q.

Theorem leb_le p q : (p <=? q) = true <-> p <= q.

Include BoolEqualityFacts.

Definition switch_Eq c c´ :=
 match c´ with
  | Eq => c
  | Lt => Lt
  | Gt => Gt
 end.

Lemma compare_cont_spec p q c :
  compare_cont p q c = switch_Eq c (p ?= q).

Theorem compare_cont_Eq p q c :
 compare_cont p q c = Eq -> c = Eq.

Lemma compare_cont_Lt_Gt p q :
  compare_cont p q Lt = Gt <-> p > q.

Lemma compare_cont_Lt_Lt p q :
  compare_cont p q Lt = Lt <-> p <= q.

Lemma compare_cont_Gt_Lt p q :
  compare_cont p q Gt = Lt <-> p < q.

Lemma compare_cont_Gt_Gt p q :
  compare_cont p q Gt = Gt <-> p >= q.

Lemma compare_xO_xO p q : (p~0 ?= q~0) = (p ?= q).

Lemma compare_xI_xI p q : (p~1 ?= q~1) = (p ?= q).

Lemma compare_xI_xO p q :
 (p~1 ?= q~0) = switch_Eq Gt (p ?= q).

Lemma compare_xO_xI p q :
 (p~0 ?= q~1) = switch_Eq Lt (p ?= q).

Hint Rewrite compare_xO_xO compare_xI_xI compare_xI_xO compare_xO_xI : compare.

Ltac simpl_compare := autorewrite with compare.
Ltac simpl_compare_in H := autorewrite with compare in H.

Definition mask2cmp (p:mask) : comparison :=
 match p with
  | IsNul => Eq
  | IsPos _ => Gt
  | IsNeg => Lt
 end.

Lemma compare_sub_mask p q : (p ?= q) = mask2cmp (sub_mask p q).

Lemma lt_iff_add p q : p < q <-> exists r, p + r = q.

Lemma gt_iff_add p q : p > q <-> exists r, q + r = p.

Theorem compare_cont_refl p c :
  compare_cont p p c = c.

Lemma compare_cont_antisym p q c :
  CompOpp (compare_cont p q c) = compare_cont q p (CompOpp c).

Lemma compare_eq_iff p q : (p ?= q) = Eq <-> p = q.

Lemma compare_antisym p q : (q ?= p) = CompOpp (p ?= q).

Lemma compare_lt_iff p q : (p ?= q) = Lt <-> p < q.

Lemma compare_le_iff p q : (p ?= q) <> Gt <-> p <= q.

Include BoolOrderFacts.

Definition le_lteq := lt_eq_cases.

Lemma gt_lt_iff p q : p > q <-> q < p.

Lemma gt_lt p q : p > q -> q < p.

Lemma lt_gt p q : p < q -> q > p.

Lemma ge_le_iff p q : p >= q <-> q <= p.

Lemma ge_le p q : p >= q -> q <= p.

Lemma le_ge p q : p <= q -> q >= p.

Lemma compare_succ_r p q :
  switch_Eq Gt (p ?= succ q) = switch_Eq Lt (p ?= q).

Lemma compare_succ_l p q :
  switch_Eq Lt (succ p ?= q) = switch_Eq Gt (p ?= q).

Theorem lt_succ_r p q : p < succ q <-> p <= q.

Lemma lt_succ_diag_r p : p < succ p.

Lemma compare_succ_succ p q : (succ p ?= succ q) = (p ?= q).

Lemma le_1_l p : 1 <= p.

Lemma nlt_1_r p : ~ p < 1.

Lemma lt_1_succ p : 1 < succ p.

Lemma le_nlt p q : p <= q <-> ~ q < p.

Lemma lt_nle p q : p < q <-> ~ q <= p.

Lemma lt_le_incl p q : p<q -> p<=q.

Lemma lt_lt_succ n m : n < m -> n < succ m.

Lemma succ_lt_mono n m : n < m <-> succ n < succ m.

Lemma succ_le_mono n m : n <= m <-> succ n <= succ m.

Lemma lt_trans n m p : n < m -> m < p -> n < p.

Theorem lt_ind : forall (A : positive -> Prop) (n : positive),
  A (succ n) ->
    (forall m : positive, n < m -> A m -> A (succ m)) ->
      forall m : positive, n < m -> A m.

Instance lt_strorder : StrictOrder lt.

Instance lt_compat : Proper (Logic.eq==>Logic.eq==>iff) lt.

Lemma lt_total p q : p < q \/ p = q \/ q < p.

Lemma le_refl p : p <= p.

Lemma le_lt_trans n m p : n <= m -> m < p -> n < p.

Lemma lt_le_trans n m p : n < m -> m <= p -> n < p.

Lemma le_trans n m p : n <= m -> m <= p -> n <= p.

Lemma le_succ_l n m : succ n <= m <-> n < m.

Lemma le_antisym p q : p <= q -> q <= p -> p = q.

Instance le_preorder : PreOrder le.

Instance le_partorder : PartialOrder Logic.eq le.

Lemma add_compare_mono_l p q r : (p+q ?= p+r) = (q ?= r).

Lemma add_compare_mono_r p q r : (q+p ?= r+p) = (q ?= r).

Lemma lt_add_diag_r p q : p < p + q.

Lemma add_lt_mono_l p q r : q<r <-> p+q < p+r.

Lemma add_lt_mono_r p q r : q<r <-> q+p < r+p.

Lemma add_lt_mono p q r s : p<q -> r<s -> p+r<q+s.

Lemma add_le_mono_l p q r : q<=r <-> p+q<=p+r.

Lemma add_le_mono_r p q r : q<=r <-> q+p<=r+p.

Lemma add_le_mono p q r s : p<=q -> r<=s -> p+r <= q+s.

Lemma mul_compare_mono_l p q r : (p*q ?= p*r) = (q ?= r).

Lemma mul_compare_mono_r p q r : (q*p ?= r*p) = (q ?= r).

Lemma mul_lt_mono_l p q r : q<r <-> p*q < p*r.

Lemma mul_lt_mono_r p q r : q<r <-> q*p < r*p.

Lemma mul_lt_mono p q r s : p<q -> r<s -> p*r < q*s.

Lemma mul_le_mono_l p q r : q<=r <-> p*q<=p*r.

Lemma mul_le_mono_r p q r : q<=r <-> q*p<=r*p.

Lemma mul_le_mono p q r s : p<=q -> r<=s -> p*r <= q*s.

Lemma lt_add_r p q : p < p+q.

Lemma lt_not_add_l p q : ~ p+q < p.

Lemma pow_gt_1 n p : 1<n -> 1<n^p.

Lemma sub_1_r p : sub p 1 = pred p.

Lemma pred_sub p : pred p = sub p 1.

Theorem sub_succ_r p q : p - (succ q) = pred (p - q).

Lemma sub_mask_pos´ p q :
  q < p -> exists r, sub_mask p q = IsPos r /\ q + r = p.

Lemma sub_mask_pos p q :
  q < p -> exists r, sub_mask p q = IsPos r.

Theorem sub_add p q : q < p -> (p-q)+q = p.

Lemma add_sub p q : (p+q)-q = p.

Lemma mul_sub_distr_l p q r : r<q -> p*(q-r) = p*q-p*r.

Lemma mul_sub_distr_r p q r : q<p -> (p-q)*r = p*r-q*r.

Lemma sub_lt_mono_l p q r: q<p -> p<r -> r-p < r-q.

Lemma sub_compare_mono_l p q r :
 q<p -> r<p -> (p-q ?= p-r) = (r ?= q).

Lemma sub_compare_mono_r p q r :
 p<q -> p<r -> (q-p ?= r-p) = (q ?= r).

Lemma sub_lt_mono_r p q r : q<p -> r<q -> q-r < p-r.

Lemma sub_decr n m : m<n -> n-m < n.

Lemma add_sub_assoc p q r : r<q -> p+(q-r) = p+q-r.

Lemma sub_add_distr p q r : q+r < p -> p-(q+r) = p-q-r.

Lemma sub_sub_distr p q r : r<q -> q-r < p -> p-(q-r) = p+r-q.

Lemma sub_xO_xO n m : m<n -> n~0 - m~0 = (n-m)~0.

Lemma sub_xI_xI n m : m<n -> n~1 - m~1 = (n-m)~0.

Lemma sub_xI_xO n m : m<n -> n~1 - m~0 = (n-m)~1.

Lemma sub_xO_xI n m : n~0 - m~1 = pred_double (n-m).

Lemma sub_mask_neg_iff´ p q : sub_mask p q = IsNeg <-> p < q.

Lemma sub_mask_neg p q : p<q -> sub_mask p q = IsNeg.

Lemma sub_le p q : p<=q -> p-q = 1.

Lemma sub_lt p q : p<q -> p-q = 1.

Lemma sub_diag p : p-p = 1.

Lemma size_nat_monotone p q : p<q -> (size_nat p <= size_nat q)%nat.

Lemma size_gt p : p < 2^(size p).

Lemma size_le p : 2^(size p) <= p~0.

Lemma max_l : forall x y, y<=x -> max x y = x.

Lemma max_r : forall x y, x<=y -> max x y = y.

Lemma min_l : forall x y, x<=y -> min x y = x.

Lemma min_r : forall x y, y<=x -> min x y = y.

Include UsualMinMaxLogicalProperties <+ UsualMinMaxDecProperties.

Ltac order := Private_Tac.order.

Lemma max_1_l n : max 1 n = n.

Lemma max_1_r n : max n 1 = n.

Lemma min_1_l n : min 1 n = 1.

Lemma min_1_r n : min n 1 = 1.

Lemma succ_max_distr n m : succ (max n m) = max (succ n) (succ m).

Lemma succ_min_distr n m : succ (min n m) = min (succ n) (succ m).

Lemma add_max_distr_l n m p : max (p + n) (p + m) = p + max n m.

Lemma add_max_distr_r n m p : max (n + p) (m + p) = max n m + p.

Lemma add_min_distr_l n m p : min (p + n) (p + m) = p + min n m.

Lemma add_min_distr_r n m p : min (n + p) (m + p) = min n m + p.

Lemma mul_max_distr_l n m p : max (p * n) (p * m) = p * max n m.

Lemma mul_max_distr_r n m p : max (n * p) (m * p) = max n m * p.

Lemma mul_min_distr_l n m p : min (p * n) (p * m) = p * min n m.

Lemma mul_min_distr_r n m p : min (n * p) (m * p) = min n m * p.

Lemma iter_op_succ : forall A (op:A->A->A),
 (forall x y z, op x (op y z) = op (op x y) z) ->
 forall p a,
 iter_op op (succ p) a = op a (iter_op op p a).

Lemma of_nat_succ (n:nat) : of_succ_nat n = of_nat (S n).

Lemma pred_of_succ_nat (n:nat) : pred (of_succ_nat n) = of_nat n.

Lemma succ_of_nat (n:nat) : n<>O -> succ (of_nat n) = of_succ_nat n.

Inductive SqrtSpec : positive*mask -> positive -> Prop :=
 | SqrtExact s x : x=s*s -> SqrtSpec (s,IsNul) x
 | SqrtApprox s r x : x=s*s+r -> r <= s~0 -> SqrtSpec (s,IsPos r) x.

Lemma sqrtrem_step_spec f g p x :
 (f=xO \/ f=xI) -> (g=xO \/ g=xI) ->
 SqrtSpec p x -> SqrtSpec (sqrtrem_step f g p) (g (f x)).

Lemma sqrtrem_spec p : SqrtSpec (sqrtrem p) p.

Lemma sqrt_spec p :
 let s := sqrt p in s*s <= p < (succ s)*(succ s).

Lemma divide_add_cancel_l p q r : (p | r) -> (p | q + r) -> (p | q).

Lemma divide_xO_xI p q r : (p | q~0) -> (p | r~1) -> (p | q).

Lemma divide_xO_xO p q : (p~0|q~0) <-> (p|q).

Lemma divide_mul_l p q r : (p|q) -> (p|q*r).

Lemma divide_mul_r p q r : (p|r) -> (p|q*r).

Lemma ggcdn_gcdn : forall n a b,
  fst (ggcdn n a b) = gcdn n a b.

Lemma ggcd_gcd : forall a b, fst (ggcd a b) = gcd a b.

Ltac destr_pggcdn IHn :=
 match goal with |- context [ ggcdn _ ?x ?y ] =>
  generalize (IHn x y); destruct ggcdn as (g,(u,v)); simpl
 end.

Lemma ggcdn_correct_divisors : forall n a b,
  let ´(g,(aa,bb)) := ggcdn n a b in
  a = g*aa /\ b = g*bb.

Lemma ggcd_correct_divisors : forall a b,
  let ´(g,(aa,bb)) := ggcd a b in
  a=g*aa /\ b=g*bb.

Lemma gcd_divide_l : forall a b, (gcd a b | a).

Lemma gcd_divide_r : forall a b, (gcd a b | b).

Lemma gcdn_greatest : forall n a b, (size_nat a + size_nat b <= n)%nat ->
 forall p, (p|a) -> (p|b) -> (p|gcdn n a b).

Lemma gcd_greatest : forall a b p, (p|a) -> (p|b) -> (p|gcd a b).

Lemma ggcd_greatest : forall a b,
 let (aa,bb) := snd (ggcd a b) in
 forall p, (p|aa) -> (p|bb) -> p=1.

End Pos.

Infix "+" := Pos.add : positive_scope.
Infix "-" := Pos.sub : positive_scope.
Infix "*" := Pos.mul : positive_scope.
Infix "^" := Pos.pow : positive_scope.
Infix "?=" := Pos.compare (at level 70, no associativity) : positive_scope.
Infix "=?" := Pos.eqb (at level 70, no associativity) : positive_scope.
Infix "<=?" := Pos.leb (at level 70, no associativity) : positive_scope.
Infix "<?" := Pos.ltb (at level 70, no associativity) : positive_scope.
Infix "<=" := Pos.le : positive_scope.
Infix "<" := Pos.lt : positive_scope.
Infix ">=" := Pos.ge : positive_scope.
Infix ">" := Pos.gt : positive_scope.

Notation "x <= y <= z" := (x <= y /\ y <= z) : positive_scope.
Notation "x <= y < z" := (x <= y /\ y < z) : positive_scope.
Notation "x < y < z" := (x < y /\ y < z) : positive_scope.
Notation "x < y <= z" := (x < y /\ y <= z) : positive_scope.

Notation "( p | q )" := (Pos.divide p q) (at level 0) : positive_scope.

Notation positive := positive (only parsing).
Notation positive_rect := positive_rect (only parsing).
Notation positive_rec := positive_rec (only parsing).
Notation positive_ind := positive_ind (only parsing).
Notation xI := xI (only parsing).
Notation xO := xO (only parsing).
Notation xH := xH (only parsing).

Notation IsNul := Pos.IsNul (only parsing).
Notation IsPos := Pos.IsPos (only parsing).
Notation IsNeg := Pos.IsNeg (only parsing).

Notation Psucc := Pos.succ (compat "8.3").
Notation Pplus := Pos.add (compat "8.3").
Notation Pplus_carry := Pos.add_carry (compat "8.3").
Notation Ppred := Pos.pred (compat "8.3").
Notation Piter_op := Pos.iter_op (compat "8.3").
Notation Piter_op_succ := Pos.iter_op_succ (compat "8.3").
Notation Pmult_nat := (Pos.iter_op plus) (compat "8.3").
Notation nat_of_P := Pos.to_nat (compat "8.3").
Notation P_of_succ_nat := Pos.of_succ_nat (compat "8.3").
Notation Pdouble_minus_one := Pos.pred_double (compat "8.3").
Notation positive_mask := Pos.mask (compat "8.3").
Notation positive_mask_rect := Pos.mask_rect (compat "8.3").
Notation positive_mask_ind := Pos.mask_ind (compat "8.3").
Notation positive_mask_rec := Pos.mask_rec (compat "8.3").
Notation Pdouble_plus_one_mask := Pos.succ_double_mask (compat "8.3").
Notation Pdouble_mask := Pos.double_mask (compat "8.3").
Notation Pdouble_minus_two := Pos.double_pred_mask (compat "8.3").
Notation Pminus_mask := Pos.sub_mask (compat "8.3").
Notation Pminus_mask_carry := Pos.sub_mask_carry (compat "8.3").
Notation Pminus := Pos.sub (compat "8.3").
Notation Pmult := Pos.mul (compat "8.3").
Notation iter_pos := @Pos.iter (compat "8.3").
Notation Ppow := Pos.pow (compat "8.3").
Notation Pdiv2 := Pos.div2 (compat "8.3").
Notation Pdiv2_up := Pos.div2_up (compat "8.3").
Notation Psize := Pos.size_nat (compat "8.3").
Notation Psize_pos := Pos.size (compat "8.3").
Notation Pcompare := Pos.compare_cont (compat "8.3").
Notation Plt := Pos.lt (compat "8.3").
Notation Pgt := Pos.gt (compat "8.3").
Notation Ple := Pos.le (compat "8.3").
Notation Pge := Pos.ge (compat "8.3").
Notation Pmin := Pos.min (compat "8.3").
Notation Pmax := Pos.max (compat "8.3").
Notation Peqb := Pos.eqb (compat "8.3").
Notation positive_eq_dec := Pos.eq_dec (compat "8.3").
Notation xI_succ_xO := Pos.xI_succ_xO (compat "8.3").
Notation Psucc_discr := Pos.succ_discr (compat "8.3").
Notation Psucc_o_double_minus_one_eq_xO :=
 Pos.succ_pred_double (compat "8.3").
Notation Pdouble_minus_one_o_succ_eq_xI :=
 Pos.pred_double_succ (compat "8.3").
Notation xO_succ_permute := Pos.double_succ (compat "8.3").
Notation double_moins_un_xO_discr :=
 Pos.pred_double_xO_discr (compat "8.3").
Notation Psucc_not_one := Pos.succ_not_1 (compat "8.3").
Notation Ppred_succ := Pos.pred_succ (compat "8.3").
Notation Psucc_pred := Pos.succ_pred_or (compat "8.3").
Notation Psucc_inj := Pos.succ_inj (compat "8.3").
Notation Pplus_carry_spec := Pos.add_carry_spec (compat "8.3").
Notation Pplus_comm := Pos.add_comm (compat "8.3").
Notation Pplus_succ_permute_r := Pos.add_succ_r (compat "8.3").
Notation Pplus_succ_permute_l := Pos.add_succ_l (compat "8.3").
Notation Pplus_no_neutral := Pos.add_no_neutral (compat "8.3").
Notation Pplus_carry_plus := Pos.add_carry_add (compat "8.3").
Notation Pplus_reg_r := Pos.add_reg_r (compat "8.3").
Notation Pplus_reg_l := Pos.add_reg_l (compat "8.3").
Notation Pplus_carry_reg_r := Pos.add_carry_reg_r (compat "8.3").
Notation Pplus_carry_reg_l := Pos.add_carry_reg_l (compat "8.3").
Notation Pplus_assoc := Pos.add_assoc (compat "8.3").
Notation Pplus_xO := Pos.add_xO (compat "8.3").
Notation Pplus_xI_double_minus_one := Pos.add_xI_pred_double (compat "8.3").
Notation Pplus_xO_double_minus_one := Pos.add_xO_pred_double (compat "8.3").
Notation Pplus_diag := Pos.add_diag (compat "8.3").
Notation PeanoView := Pos.PeanoView (compat "8.3").
Notation PeanoOne := Pos.PeanoOne (compat "8.3").
Notation PeanoSucc := Pos.PeanoSucc (compat "8.3").
Notation PeanoView_rect := Pos.PeanoView_rect (compat "8.3").
Notation PeanoView_ind := Pos.PeanoView_ind (compat "8.3").
Notation PeanoView_rec := Pos.PeanoView_rec (compat "8.3").
Notation peanoView_xO := Pos.peanoView_xO (compat "8.3").
Notation peanoView_xI := Pos.peanoView_xI (compat "8.3").
Notation peanoView := Pos.peanoView (compat "8.3").
Notation PeanoView_iter := Pos.PeanoView_iter (compat "8.3").
Notation eq_dep_eq_positive := Pos.eq_dep_eq_positive (compat "8.3").
Notation PeanoViewUnique := Pos.PeanoViewUnique (compat "8.3").
Notation Prect := Pos.peano_rect (compat "8.3").
Notation Prect_succ := Pos.peano_rect_succ (compat "8.3").
Notation Prect_base := Pos.peano_rect_base (compat "8.3").
Notation Prec := Pos.peano_rec (compat "8.3").
Notation Pind := Pos.peano_ind (compat "8.3").
Notation Pcase := Pos.peano_case (compat "8.3").
Notation Pmult_1_r := Pos.mul_1_r (compat "8.3").
Notation Pmult_Sn_m := Pos.mul_succ_l (compat "8.3").
Notation Pmult_xO_permute_r := Pos.mul_xO_r (compat "8.3").
Notation Pmult_xI_permute_r := Pos.mul_xI_r (compat "8.3").
Notation Pmult_comm := Pos.mul_comm (compat "8.3").
Notation Pmult_plus_distr_l := Pos.mul_add_distr_l (compat "8.3").
Notation Pmult_plus_distr_r := Pos.mul_add_distr_r (compat "8.3").
Notation Pmult_assoc := Pos.mul_assoc (compat "8.3").
Notation Pmult_xI_mult_xO_discr := Pos.mul_xI_mul_xO_discr (compat "8.3").
Notation Pmult_xO_discr := Pos.mul_xO_discr (compat "8.3").
Notation Pmult_reg_r := Pos.mul_reg_r (compat "8.3").
Notation Pmult_reg_l := Pos.mul_reg_l (compat "8.3").
Notation Pmult_1_inversion_l := Pos.mul_eq_1_l (compat "8.3").
Notation Psquare_xO := Pos.square_xO (compat "8.3").
Notation Psquare_xI := Pos.square_xI (compat "8.3").
Notation iter_pos_swap_gen := Pos.iter_swap_gen (compat "8.3").
Notation iter_pos_swap := Pos.iter_swap (compat "8.3").
Notation iter_pos_succ := Pos.iter_succ (compat "8.3").
Notation iter_pos_plus := Pos.iter_add (compat "8.3").
Notation iter_pos_invariant := Pos.iter_invariant (compat "8.3").
Notation Ppow_1_r := Pos.pow_1_r (compat "8.3").
Notation Ppow_succ_r := Pos.pow_succ_r (compat "8.3").
Notation Peqb_refl := Pos.eqb_refl (compat "8.3").
Notation Peqb_eq := Pos.eqb_eq (compat "8.3").
Notation Pcompare_refl_id := Pos.compare_cont_refl (compat "8.3").
Notation Pcompare_eq_iff := Pos.compare_eq_iff (compat "8.3").
Notation Pcompare_Gt_Lt := Pos.compare_cont_Gt_Lt (compat "8.3").
Notation Pcompare_eq_Lt := Pos.compare_lt_iff (compat "8.3").
Notation Pcompare_Lt_Gt := Pos.compare_cont_Lt_Gt (compat "8.3").

Notation Pcompare_antisym := Pos.compare_cont_antisym (compat "8.3").
Notation ZC1 := Pos.gt_lt (compat "8.3").
Notation ZC2 := Pos.lt_gt (compat "8.3").
Notation Pcompare_spec := Pos.compare_spec (compat "8.3").
Notation Pcompare_p_Sp := Pos.lt_succ_diag_r (compat "8.3").
Notation Pcompare_succ_succ := Pos.compare_succ_succ (compat "8.3").
Notation Pcompare_1 := Pos.nlt_1_r (compat "8.3").
Notation Plt_1 := Pos.nlt_1_r (compat "8.3").
Notation Plt_1_succ := Pos.lt_1_succ (compat "8.3").
Notation Plt_lt_succ := Pos.lt_lt_succ (compat "8.3").
Notation Plt_irrefl := Pos.lt_irrefl (compat "8.3").
Notation Plt_trans := Pos.lt_trans (compat "8.3").
Notation Plt_ind := Pos.lt_ind (compat "8.3").
Notation Ple_lteq := Pos.le_lteq (compat "8.3").
Notation Ple_refl := Pos.le_refl (compat "8.3").
Notation Ple_lt_trans := Pos.le_lt_trans (compat "8.3").
Notation Plt_le_trans := Pos.lt_le_trans (compat "8.3").
Notation Ple_trans := Pos.le_trans (compat "8.3").
Notation Plt_succ_r := Pos.lt_succ_r (compat "8.3").
Notation Ple_succ_l := Pos.le_succ_l (compat "8.3").
Notation Pplus_compare_mono_l := Pos.add_compare_mono_l (compat "8.3").
Notation Pplus_compare_mono_r := Pos.add_compare_mono_r (compat "8.3").
Notation Pplus_lt_mono_l := Pos.add_lt_mono_l (compat "8.3").
Notation Pplus_lt_mono_r := Pos.add_lt_mono_r (compat "8.3").
Notation Pplus_lt_mono := Pos.add_lt_mono (compat "8.3").
Notation Pplus_le_mono_l := Pos.add_le_mono_l (compat "8.3").
Notation Pplus_le_mono_r := Pos.add_le_mono_r (compat "8.3").
Notation Pplus_le_mono := Pos.add_le_mono (compat "8.3").
Notation Pmult_compare_mono_l := Pos.mul_compare_mono_l (compat "8.3").
Notation Pmult_compare_mono_r := Pos.mul_compare_mono_r (compat "8.3").
Notation Pmult_lt_mono_l := Pos.mul_lt_mono_l (compat "8.3").
Notation Pmult_lt_mono_r := Pos.mul_lt_mono_r (compat "8.3").
Notation Pmult_lt_mono := Pos.mul_lt_mono (compat "8.3").
Notation Pmult_le_mono_l := Pos.mul_le_mono_l (compat "8.3").
Notation Pmult_le_mono_r := Pos.mul_le_mono_r (compat "8.3").
Notation Pmult_le_mono := Pos.mul_le_mono (compat "8.3").
Notation Plt_plus_r := Pos.lt_add_r (compat "8.3").
Notation Plt_not_plus_l := Pos.lt_not_add_l (compat "8.3").
Notation Ppow_gt_1 := Pos.pow_gt_1 (compat "8.3").
Notation Ppred_mask := Pos.pred_mask (compat "8.3").
Notation Pminus_mask_succ_r := Pos.sub_mask_succ_r (compat "8.3").
Notation Pminus_mask_carry_spec := Pos.sub_mask_carry_spec (compat "8.3").
Notation Pminus_succ_r := Pos.sub_succ_r (compat "8.3").
Notation Pminus_mask_diag := Pos.sub_mask_diag (compat "8.3").

Notation Pplus_minus_eq := Pos.add_sub (compat "8.3").
Notation Pmult_minus_distr_l := Pos.mul_sub_distr_l (compat "8.3").
Notation Pminus_lt_mono_l := Pos.sub_lt_mono_l (compat "8.3").
Notation Pminus_compare_mono_l := Pos.sub_compare_mono_l (compat "8.3").
Notation Pminus_compare_mono_r := Pos.sub_compare_mono_r (compat "8.3").
Notation Pminus_lt_mono_r := Pos.sub_lt_mono_r (compat "8.3").
Notation Pminus_decr := Pos.sub_decr (compat "8.3").
Notation Pminus_xI_xI := Pos.sub_xI_xI (compat "8.3").
Notation Pplus_minus_assoc := Pos.add_sub_assoc (compat "8.3").
Notation Pminus_plus_distr := Pos.sub_add_distr (compat "8.3").
Notation Pminus_minus_distr := Pos.sub_sub_distr (compat "8.3").
Notation Pminus_mask_Lt := Pos.sub_mask_neg (compat "8.3").
Notation Pminus_Lt := Pos.sub_lt (compat "8.3").
Notation Pminus_Eq := Pos.sub_diag (compat "8.3").
Notation Psize_monotone := Pos.size_nat_monotone (compat "8.3").
Notation Psize_pos_gt := Pos.size_gt (compat "8.3").
Notation Psize_pos_le := Pos.size_le (compat "8.3").