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. Style: centered; floating; windowed.
(* -*- coding: utf-8 -*- *)
(************************************************************************)
(*         *   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 Export BinNums.
Require Import Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid
 Equalities Orders OrdersFacts GenericMinMax Le Plus.

Require Export BinPosDef.

(**********************************************************************)

Binary positive numbers, operations and properties

(**********************************************************************)
Initial development by Pierre Crégut, CNET, Lannion, France
The type positive and its constructors xI and xO and xH are now defined in BinNums.v
Local Open Scope positive_scope.
Every definitions and early properties about positive numbers are placed in a module Pos for qualification purpose.
Module Pos
 <: UsualOrderedTypeFull
 <: UsualDecidableTypeFull
 <: TotalOrder.

Definitions of operations, now in a separate file

Include BinPosDef.Pos.
In functor applications that follow, we only inline t and eq
Set Inline Level 30.

Logical Predicates

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.

(**********************************************************************)

Properties of operations over positive numbers

Decidability of equality on binary positive numbers


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

forall x y : positive, {x = y} + {x <> y}
decide equality. Defined. (**********************************************************************)

Properties of successor on binary positive numbers

Specification of xI in term of succ and xO

p:positive

p~1 = succ p~0
p:positive

p~1 = succ p~0
reflexivity. Qed.
p:positive

p <> succ p
p:positive

p <> succ p
now destruct p. Qed.

Successor and double

p:positive

pred_double p = pred p~0
p:positive

pred_double p = pred p~0
reflexivity. Qed.
p:positive

succ (pred_double p) = p~0
p:positive

succ (pred_double p) = p~0
induction p; simpl; now f_equal. Qed.
p:positive

pred_double (succ p) = p~1
p:positive

pred_double (succ p) = p~1
induction p; simpl; now f_equal. Qed.
p:positive

(succ p)~0 = succ (succ p~0)
p:positive

(succ p)~0 = succ (succ p~0)
now destruct p. Qed.
p:positive

pred_double p <> p~0
p:positive

pred_double p <> p~0
now destruct p. Qed.

Successor and predecessor

p:positive

succ p <> 1
p:positive

succ p <> 1
now destruct p. Qed.
p:positive

pred (succ p) = p
p:positive

pred (succ p) = p
p:positive

pred_double (succ p) = p~1
apply pred_double_succ. Qed.
p:positive

p = 1 \/ succ (pred p) = p
p:positive

p = 1 \/ succ (pred p) = p
p:positive

p~0 = 1 \/ succ (pred_double p) = p~0
right; apply succ_pred_double. Qed.
p:positive

p <> 1 -> succ (pred p) = p
p:positive

p <> 1 -> succ (pred p) = p
p:positive
H:p~0 <> 1

succ (pred_double p) = p~0
H:1 <> 1
2 = 1
H:1 <> 1

2 = 1
now destruct H. Qed.

Injectivity of successor

p, q:positive

succ p = succ q -> p = q
p, q:positive

succ p = succ q -> p = q
p:positive

forall q : positive, succ p = succ q -> p = q
p:positive
IHp:forall q : positive, succ p = succ q -> p = q
H:succ p = 1

p~1 = 1
q:positive
H:1 = succ q
1 = q~1
q:positive
H:1 = succ q

1 = q~1
elim (succ_not_1 q); auto. Qed.

Predecessor to N

p:positive

pred_N (succ p) = Npos p
p:positive

pred_N (succ p) = Npos p
p:positive

Npos (pred_double (succ p)) = Npos p~1
p:positive

pred_double (succ p) = p~1
apply pred_double_succ. Qed. (**********************************************************************)

Properties of addition on binary positive numbers

Specification of succ in term of add

p:positive

p + 1 = succ p
p:positive

p + 1 = succ p
now destruct p. Qed.
p:positive

1 + p = succ p
p:positive

1 + p = succ p
now destruct p. Qed.

Specification of add_carry

p, q:positive

add_carry p q = succ (p + q)
p, q:positive

add_carry p q = succ (p + q)
p:positive

forall q : positive, add_carry p q = succ (p + q)
induction p; destruct q; simpl; now f_equal. Qed.

Commutativity

p, q:positive

p + q = q + p
p, q:positive

p + q = q + p
p:positive

forall q : positive, p + q = q + p
p:positive
IHp:forall q0 : positive, p + q0 = q0 + p
q:positive

add_carry p q = add_carry q p
rewrite 2 add_carry_spec; now f_equal. Qed.

Permutation of add and succ

p, q:positive

p + succ q = succ (p + q)
p, q:positive

p + succ q = succ (p + q)
p:positive

forall q : positive, p + succ q = succ (p + q)
induction p; destruct q; simpl; f_equal; auto using add_1_r; rewrite add_carry_spec; auto. Qed.
p, q:positive

succ p + q = succ (p + q)
p, q:positive

succ p + q = succ (p + q)
p, q:positive

q + succ p = succ (q + p)
apply add_succ_r. Qed.

No neutral elements for addition

p, q:positive

q + p <> p
p, q:positive

q + p <> p
p:positive

forall q : positive, q + p <> p
induction p as [p IHp|p IHp| ]; intros [q|q| ] H; destr_eq H; apply (IHp q H). Qed.

Simplification

p, q, r, s:positive

add_carry p r = add_carry q s -> p + r = q + s
p, q, r, s:positive

add_carry p r = add_carry q s -> p + r = q + s
intros H; apply succ_inj; now rewrite <- 2 add_carry_spec. Qed.
p, q, r:positive

p + r = q + r -> p = q
p, q, r:positive

p + r = q + r -> p = q
r:positive

forall p q : positive, p + r = q + r -> p = q
r:positive
IHr:forall p q : positive, p + r = q + r -> p = q

forall p q : positive, p + r~1 = q + r~1 -> p = q
r:positive
IHr:forall p q : positive, p + r = q + r -> p = q
forall p q : positive, p + r~0 = q + r~0 -> p = q

forall p q : positive, p + 1 = q + 1 -> p = q
r:positive
IHr:forall p q : positive, p + r = q + r -> p = q

forall p q : positive, p + r~0 = q + r~0 -> p = q

forall p q : positive, p + 1 = q + 1 -> p = q

forall p q : positive, p + 1 = q + 1 -> p = q
p, q:positive
H:p + 1 = q + 1

p = q
p, q:positive
H:p + 1 = q + 1

succ p = succ q
now rewrite <- 2 add_1_r. Qed.
p, q, r:positive

p + q = p + r -> q = r
p, q, r:positive

p + q = p + r -> q = r
p, q, r:positive

q + p = r + p -> q = r
now apply add_reg_r. Qed.
p, q, r:positive

p + r = q + r <-> p = q
p, q, r:positive

p + r = q + r <-> p = q
p, q, r:positive

p + r = q + r -> p = q
p, q, r:positive
p = q -> p + r = q + r
p, q, r:positive

p = q -> p + r = q + r
congruence. Qed.
p, q, r:positive

r + p = r + q <-> p = q
p, q, r:positive

r + p = r + q <-> p = q
p, q, r:positive

r + p = r + q -> p = q
p, q, r:positive
p = q -> r + p = r + q
p, q, r:positive

p = q -> r + p = r + q
congruence. Qed.
p, q, r:positive

add_carry p r = add_carry q r -> p = q
p, q, r:positive

add_carry p r = add_carry q r -> p = q
p, q, r:positive
H:add_carry p r = add_carry q r

p = q
apply add_reg_r with (r:=r); now apply add_carry_add. Qed.
p, q, r:positive

add_carry p q = add_carry p r -> q = r
p, q, r:positive

add_carry p q = add_carry p r -> q = r
intros H; apply add_reg_r with (r:=p); rewrite (add_comm r), (add_comm q); now apply add_carry_add. Qed.

Addition is associative

p, q, r:positive

p + (q + r) = p + q + r
p, q, r:positive

p + (q + r) = p + q + r
p:positive

forall q r : positive, p + (q + r) = p + q + r
p:positive
IHp:forall q r : positive, p + (q + r) = p + q + r

forall q r : positive, p~1 + (q + r) = p~1 + q + r
p:positive
IHp:forall q r : positive, p + (q + r) = p + q + r
forall q r : positive, p~0 + (q + r) = p~0 + q + r

forall q r : positive, 1 + (q + r) = 1 + q + r
p:positive
IHp:forall q r : positive, p + (q + r) = p + q + r

forall q r : positive, p~0 + (q + r) = p~0 + q + r

forall q r : positive, 1 + (q + r) = 1 + q + r

forall q r : positive, 1 + (q + r) = 1 + q + r
intros q r; rewrite 2 add_1_l, add_succ_l; auto. Qed.

Commutation of addition and double

p, q:positive

(p + q)~0 = p~0 + q~0
p, q:positive

(p + q)~0 = p~0 + q~0
now destruct p, q. Qed.
p, q:positive

(p + q)~0 = p~1 + pred_double q
p, q:positive

(p + q)~0 = p~1 + pred_double q
p, q:positive

(p + q)~0 = p~0 + 1 + pred_double q
now rewrite <- add_assoc, add_1_l, succ_pred_double. Qed.
p, q:positive

pred_double (p + q) = p~0 + pred_double q
p, q:positive

pred_double (p + q) = p~0 + pred_double q
p:positive

forall q : positive, pred_double (p + q) = p~0 + pred_double q
p:positive
IHp:forall q0 : positive, pred_double (p + q0) = p~0 + pred_double q0
q:positive

(pred_double (p + q))~1 = match pred_double q with | q0~1 => (p + q0)~1 | q0~0 => (p + q0)~0 | 1 => p~1 end~1
q:positive
q~0~1 = match pred_double q with | q0~1 => (succ q0)~0 | q0~0 => q0~1 | 1 => 2 end~1
q:positive

q~0~1 = match pred_double q with | q0~1 => (succ q0)~0 | q0~0 => q0~1 | 1 => 2 end~1
q:positive

(1 + pred_double q)~1 = match pred_double q with | q0~1 => (succ q0)~0 | q0~0 => q0~1 | 1 => 2 end~1
reflexivity. Qed.

Miscellaneous

p:positive

p + p = p~0
p:positive

p + p = p~0
induction p as [p IHp| p IHp| ]; simpl; now rewrite ?add_carry_spec, ?IHp. Qed. (**********************************************************************)

Peano induction and recursion on binary positive positive numbers

The Peano-like recursor function for positive (due to Daniel Schepler)
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.

P:positive -> Type
a:P 1
f:forall p0 : positive, P p0 -> P (succ p0)
p:positive

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

peano_rect P a f (succ p) = f p (peano_rect P a f p)
p:positive

forall (P : positive -> Type) (a : P 1) (f : forall p0 : positive, P p0 -> P (succ p0)), peano_rect P a f (succ p) = f p (peano_rect P a f p)
p:positive
IHp:forall (P : positive -> Type) (a : P 1) (f : forall p0 : positive, P p0 -> P (succ p0)), peano_rect P a f (succ p) = f p (peano_rect P a f p)

forall (P : positive -> Type) (a : P 1) (f : forall p0 : positive, P p0 -> P (succ p0)), peano_rect P a f (succ p~1) = f p~1 (peano_rect P a f p~1)
p:positive
IHp:forall (P0 : positive -> Type) (a0 : P0 1) (f0 : forall p0 : positive, P0 p0 -> P0 (succ p0)), peano_rect P0 a0 f0 (succ p) = f0 p (peano_rect P0 a0 f0 p)
P:positive -> Type
a:P 1
f:forall p0 : positive, P p0 -> P (succ p0)

peano_rect P a f (succ p~1) = f p~1 (peano_rect P a f p~1)
p:positive
IHp:forall (P0 : positive -> Type) (a0 : P0 1) (f0 : forall p0 : positive, P0 p0 -> P0 (succ p0)), peano_rect P0 a0 f0 (succ p) = f0 p (peano_rect P0 a0 f0 p)
P:positive -> Type
a:P 1
f:forall p0 : positive, P p0 -> P (succ p0)

peano_rect (fun p0 : positive => P p0~0) (f 1 a) (fun (p0 : positive) (x : P p0~0) => f p0~1 (f p0~0 x)) (succ p) = f p~1 (f p~0 (peano_rect (fun p0 : positive => P p0~0) (f 1 a) (fun (p0 : positive) (x : P p0~0) => f p0~1 (f p0~0 x)) p))
now rewrite IHp. Qed.
P:positive -> Type
a:P 1
f:forall p : positive, P p -> P (succ p)

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

peano_rect P a f 1 = a
trivial. Qed. Definition peano_rec (P:positive->Set) := peano_rect P.
Peano induction
Definition peano_ind (P:positive->Prop) := peano_rect P.
Peano case analysis

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

forall P : positive -> Prop, P 1 -> (forall n : positive, P (succ n)) -> forall p : positive, P p
intros; apply peano_ind; auto. Qed.
Earlier, the Peano-like recursor was built and proved in a way due to Conor McBride, see "The view from the left"
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).


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

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

forall x y : positive, {x = y} + {x <> y}
decide equality. Qed.

forall (p : positive) (q q' : PeanoView p), q = q'

forall (p : positive) (q q' : PeanoView p), q = q'
p:positive
q, q':PeanoView p

q = q'
q':PeanoView 1

PeanoOne = q'
p:positive
q:PeanoView p
q':PeanoView (succ p)
IHq:forall q'0 : PeanoView p, q = q'0
PeanoSucc p q = q'
q':PeanoView 1

eq_dep positive PeanoView 1 PeanoOne 1 q'
p:positive
q:PeanoView p
q':PeanoView (succ p)
IHq:forall q'0 : PeanoView p, q = q'0
PeanoSucc p q = q'
q':PeanoView 1

1 = 1 -> eq_dep positive PeanoView 1 PeanoOne 1 q'
q':PeanoView 1
1 = 1
p:positive
q:PeanoView p
q':PeanoView (succ p)
IHq:forall q'0 : PeanoView p, q = q'0
PeanoSucc p q = q'
q':PeanoView 1

(fun (p : positive) (p0 : PeanoView p) => p = 1 -> eq_dep positive PeanoView 1 PeanoOne p p0) 1 q'
q':PeanoView 1
1 = 1
p:positive
q:PeanoView p
q':PeanoView (succ p)
IHq:forall q'0 : PeanoView p, q = q'0
PeanoSucc p q = q'

1 = 1 -> eq_dep positive PeanoView 1 PeanoOne 1 PeanoOne
p:positive
q':PeanoView p
succ p = 1 -> eq_dep positive PeanoView 1 PeanoOne (succ p) (PeanoSucc p q')
q':PeanoView 1
1 = 1
p:positive
q:PeanoView p
q':PeanoView (succ p)
IHq:forall q'0 : PeanoView p, q = q'0
PeanoSucc p q = q'
p:positive
q':PeanoView p

succ p = 1 -> eq_dep positive PeanoView 1 PeanoOne (succ p) (PeanoSucc p q')
q':PeanoView 1
1 = 1
p:positive
q:PeanoView p
q':PeanoView (succ p)
IHq:forall q'0 : PeanoView p, q = q'0
PeanoSucc p q = q'
q':PeanoView 1

1 = 1
p:positive
q:PeanoView p
q':PeanoView (succ p)
IHq:forall q'0 : PeanoView p, q = q'0
PeanoSucc p q = q'
p:positive
q:PeanoView p
q':PeanoView (succ p)
IHq:forall q'0 : PeanoView p, q = q'0

PeanoSucc p q = q'
p:positive
q:PeanoView p
q':PeanoView (succ p)
IHq:forall q'0 : PeanoView p, q = q'0

eq_dep positive PeanoView (succ p) (PeanoSucc p q) (succ p) q'
p:positive
q:PeanoView p
q':PeanoView (succ p)
IHq:forall q'0 : PeanoView p, q = q'0

succ p = succ p -> eq_dep positive PeanoView (succ p) (PeanoSucc p q) (succ p) q'
p:positive
q:PeanoView p
q':PeanoView (succ p)
IHq:forall q'0 : PeanoView p, q = q'0
succ p = succ p
p:positive
q:PeanoView p
q':PeanoView (succ p)
IHq:forall q'0 : PeanoView p, q = q'0

(fun (p0 : positive) (p1 : PeanoView p0) => p0 = succ p -> eq_dep positive PeanoView (succ p) (PeanoSucc p q) p0 p1) (succ p) q'
p:positive
q:PeanoView p
q':PeanoView (succ p)
IHq:forall q'0 : PeanoView p, q = q'0
succ p = succ p
p:positive
q:PeanoView p
IHq:forall q' : PeanoView p, q = q'

1 = succ p -> eq_dep positive PeanoView (succ p) (PeanoSucc p q) 1 PeanoOne
p:positive
q:PeanoView p
p0:positive
q':PeanoView p0
IHq:forall q'0 : PeanoView p, q = q'0
succ p0 = succ p -> eq_dep positive PeanoView (succ p) (PeanoSucc p q) (succ p0) (PeanoSucc p0 q')
p:positive
q:PeanoView p
q':PeanoView (succ p)
IHq:forall q'0 : PeanoView p, q = q'0
succ p = succ p
p:positive
q:PeanoView p
IHq:forall q' : PeanoView p, q = q'
H:1 = succ p

eq_dep positive PeanoView (succ p) (PeanoSucc p q) 1 PeanoOne
p:positive
q:PeanoView p
p0:positive
q':PeanoView p0
IHq:forall q'0 : PeanoView p, q = q'0
succ p0 = succ p -> eq_dep positive PeanoView (succ p) (PeanoSucc p q) (succ p0) (PeanoSucc p0 q')
p:positive
q:PeanoView p
q':PeanoView (succ p)
IHq:forall q'0 : PeanoView p, q = q'0
succ p = succ p
p:positive
q:PeanoView p
p0:positive
q':PeanoView p0
IHq:forall q'0 : PeanoView p, q = q'0

succ p0 = succ p -> eq_dep positive PeanoView (succ p) (PeanoSucc p q) (succ p0) (PeanoSucc p0 q')
p:positive
q:PeanoView p
q':PeanoView (succ p)
IHq:forall q'0 : PeanoView p, q = q'0
succ p = succ p
p:positive
q:PeanoView p
p0:positive
q':PeanoView p0
IHq:forall q'0 : PeanoView p, q = q'0
H:succ p0 = succ p

eq_dep positive PeanoView (succ p) (PeanoSucc p q) (succ p0) (PeanoSucc p0 q')
p:positive
q:PeanoView p
q':PeanoView (succ p)
IHq:forall q'0 : PeanoView p, q = q'0
succ p = succ p
p:positive
q:PeanoView p
p0:positive
q':PeanoView p0
IHq:forall q'0 : PeanoView p, q = q'0
H:p0 = p

eq_dep positive PeanoView (succ p) (PeanoSucc p q) (succ p0) (PeanoSucc p0 q')
p:positive
q:PeanoView p
q':PeanoView (succ p)
IHq:forall q'0 : PeanoView p, q = q'0
succ p = succ p
p:positive
q:PeanoView p
p0:positive
q':PeanoView p0
IHq:forall q'0 : PeanoView p, q = q'0
H:p0 = p

forall q'0 : PeanoView p0, eq_dep positive PeanoView (succ p) (PeanoSucc p q) (succ p0) (PeanoSucc p0 q'0)
p:positive
q:PeanoView p
q':PeanoView (succ p)
IHq:forall q'0 : PeanoView p, q = q'0
succ p = succ p
p:positive
q:PeanoView p
p0:positive
q':PeanoView p0
IHq:forall q'0 : PeanoView p, q = q'0
H:p0 = p

forall q'0 : PeanoView p, eq_dep positive PeanoView (succ p) (PeanoSucc p q) (succ p) (PeanoSucc p q'0)
p:positive
q:PeanoView p
q':PeanoView (succ p)
IHq:forall q'0 : PeanoView p, q = q'0
succ p = succ p
p:positive
q:PeanoView p
p0:positive
q':PeanoView p0
IHq:forall q'1 : PeanoView p, q = q'1
H:p0 = p
q'0:PeanoView p

eq_dep positive PeanoView (succ p) (PeanoSucc p q) (succ p) (PeanoSucc p q'0)
p:positive
q:PeanoView p
q':PeanoView (succ p)
IHq:forall q'0 : PeanoView p, q = q'0
succ p = succ p
p:positive
q:PeanoView p
p0:positive
q':PeanoView p0
IHq:forall q'1 : PeanoView p, q = q'1
H:p0 = p
q'0:PeanoView p

eq_dep positive PeanoView (succ p) (PeanoSucc p q'0) (succ p) (PeanoSucc p q'0)
p:positive
q:PeanoView p
q':PeanoView (succ p)
IHq:forall q'0 : PeanoView p, q = q'0
succ p = succ p
p:positive
q:PeanoView p
q':PeanoView (succ p)
IHq:forall q'0 : PeanoView p, q = q'0

succ p = succ p
trivial. Qed.
P:positive -> Type
a:P 1
f:forall p0 : positive, P p0 -> P (succ p0)
p:positive

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

PeanoView_iter P a f p (peanoView p) = peano_rect P a f p
p:positive

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

forall (P : positive -> Type) (a : P 1) (f : forall p : positive, P p -> P (succ p)), PeanoView_iter P a f 1 (peanoView 1) = peano_rect P a f 1
p:positive
IHp:forall (P : positive -> Type) (a : P 1) (f : forall p0 : positive, P p0 -> P (succ p0)), PeanoView_iter P a f p (peanoView p) = peano_rect P a f p
forall (P : positive -> Type) (a : P 1) (f : forall p0 : positive, P p0 -> P (succ p0)), PeanoView_iter P a f (succ p) (peanoView (succ p)) = peano_rect P a f (succ p)
p:positive
IHp:forall (P : positive -> Type) (a : P 1) (f : forall p0 : positive, P p0 -> P (succ p0)), PeanoView_iter P a f p (peanoView p) = peano_rect P a f p

forall (P : positive -> Type) (a : P 1) (f : forall p0 : positive, P p0 -> P (succ p0)), PeanoView_iter P a f (succ p) (peanoView (succ p)) = peano_rect P a f (succ p)
p:positive
IHp:forall (P0 : positive -> Type) (a0 : P0 1) (f0 : forall p0 : positive, P0 p0 -> P0 (succ p0)), PeanoView_iter P0 a0 f0 p (peanoView p) = peano_rect P0 a0 f0 p
P:positive -> Type
a:P 1
f:forall p0 : positive, P p0 -> P (succ p0)

PeanoView_iter P a f (succ p) (peanoView (succ p)) = peano_rect P a f (succ p)
p:positive
IHp:forall (P0 : positive -> Type) (a0 : P0 1) (f0 : forall p0 : positive, P0 p0 -> P0 (succ p0)), PeanoView_iter P0 a0 f0 p (peanoView p) = peano_rect P0 a0 f0 p
P:positive -> Type
a:P 1
f:forall p0 : positive, P p0 -> P (succ p0)

PeanoView_iter P a f (succ p) (peanoView (succ p)) = f p (peano_rect P a f p)
p:positive
IHp:forall (P0 : positive -> Type) (a0 : P0 1) (f0 : forall p0 : positive, P0 p0 -> P0 (succ p0)), PeanoView_iter P0 a0 f0 p (peanoView p) = peano_rect P0 a0 f0 p
P:positive -> Type
a:P 1
f:forall p0 : positive, P p0 -> P (succ p0)

PeanoView_iter P a f (succ p) (PeanoSucc p (peanoView p)) = f p (peano_rect P a f p)
simpl; now f_equal. Qed. (**********************************************************************)

Properties of multiplication on binary positive numbers

One is neutral for multiplication

p:positive

1 * p = p
p:positive

1 * p = p
reflexivity. Qed.
p:positive

p * 1 = p
p:positive

p * 1 = p
induction p; simpl; now f_equal. Qed.

Right reduction properties for multiplication

p, q:positive

p * q~0 = (p * q)~0
p, q:positive

p * q~0 = (p * q)~0
induction p; simpl; f_equal; f_equal; trivial. Qed.
p, q:positive

p * q~1 = p + (p * q)~0
p, q:positive

p * q~1 = p + (p * q)~0
p, q:positive
IHp:p * q~1 = p + (p * q)~0

q + p * q~1 = p + (q + (p * q)~0)
now rewrite IHp, 2 add_assoc, (add_comm p). Qed.

Commutativity of multiplication

p, q:positive

p * q = q * p
p, q:positive

p * q = q * p
induction q as [q IHq|q IHq| ]; simpl; rewrite <- ? IHq; auto using mul_xI_r, mul_xO_r, mul_1_r. Qed.

Distributivity of multiplication over addition

p, q, r:positive

p * (q + r) = p * q + p * r
p, q, r:positive

p * (q + r) = p * q + p * r
p, q, r:positive
IHp:p * (q + r) = p * q + p * r

q + r + (p * (q + r))~0 = q + (p * q)~0 + (r + (p * r)~0)
p, q, r:positive
IHp:p * (q + r) = p * q + p * r
(p * (q + r))~0 = (p * q + p * r)~0
q, r:positive
q + r = q + r
p, q, r:positive
IHp:p * (q + r) = p * q + p * r

q + r + (p * q + p * r)~0 = q + (p * q)~0 + (r + (p * r)~0)
p, q, r:positive
IHp:p * (q + r) = p * q + p * r
(p * (q + r))~0 = (p * q + p * r)~0
q, r:positive
q + r = q + r
p, q, r:positive
IHp:p * (q + r) = p * q + p * r
m:=(p * q)~0:positive

q + r + (p * q + p * r)~0 = q + m + (r + (p * r)~0)
p, q, r:positive
IHp:p * (q + r) = p * q + p * r
(p * (q + r))~0 = (p * q + p * r)~0
q, r:positive
q + r = q + r
p, q, r:positive
IHp:p * (q + r) = p * q + p * r
m:=(p * q)~0:positive
n:=(p * r)~0:positive

q + r + (p * q + p * r)~0 = q + m + (r + n)
p, q, r:positive
IHp:p * (q + r) = p * q + p * r
(p * (q + r))~0 = (p * q + p * r)~0
q, r:positive
q + r = q + r
p, q, r:positive
IHp:p * (q + r) = p * q + p * r
m:=(p * q)~0:positive
n:=(p * r)~0:positive

q + r + (m + n) = q + m + (r + n)
p, q, r:positive
IHp:p * (q + r) = p * q + p * r
(p * (q + r))~0 = (p * q + p * r)~0
q, r:positive
q + r = q + r
p, q, r:positive
IHp:p * (q + r) = p * q + p * r
m:=(p * q)~0:positive
n:=(p * r)~0:positive

q + r + m = q + m + r
p, q, r:positive
IHp:p * (q + r) = p * q + p * r
(p * (q + r))~0 = (p * q + p * r)~0
q, r:positive
q + r = q + r
p, q, r:positive
IHp:p * (q + r) = p * q + p * r
m:=(p * q)~0:positive
n:=(p * r)~0:positive

r + m = m + r
p, q, r:positive
IHp:p * (q + r) = p * q + p * r
(p * (q + r))~0 = (p * q + p * r)~0
q, r:positive
q + r = q + r
p, q, r:positive
IHp:p * (q + r) = p * q + p * r

(p * (q + r))~0 = (p * q + p * r)~0
q, r:positive
q + r = q + r
q, r:positive

q + r = q + r
reflexivity. Qed.
p, q, r:positive

(p + q) * r = p * r + q * r
p, q, r:positive

(p + q) * r = p * r + q * r
rewrite 3 (mul_comm _ r); apply mul_add_distr_l. Qed.

Associativity of multiplication

p, q, r:positive

p * (q * r) = p * q * r
p, q, r:positive

p * (q * r) = p * q * r
p, q, r:positive
IHp:p * (q * r) = p * q * r

q * r + (p * q * r)~0 = (q + (p * q)~0) * r
now rewrite mul_add_distr_r. Qed.

Successor and multiplication

p, q:positive

succ p * q = q + p * q
p, q:positive

succ p * q = q + p * q
p, q:positive
IHp:succ p * q = q + p * q

(succ p * q)~0 = q + (q + (p * q)~0)
q:positive
q~0 = q + q
q:positive

q~0 = q + q
symmetry; apply add_diag. Qed.
p, q:positive

p * succ q = p + p * q
p, q:positive

p * succ q = p + p * q
p, q:positive

p + q * p = p + p * q
p, q:positive

q * p = p * q
apply mul_comm. Qed.

Parity properties of multiplication

p, q, r:positive

p~1 * r <> q~0 * r
p, q, r:positive

p~1 * r <> q~0 * r
p, q, r:positive
IHr:p~1 * r <> q~0 * r

p~1 * r~0 <> q~0 * r~0
rewrite 2 mul_xO_r; intro H; destr_eq H; auto. Qed.
p, q:positive

p~0 * q <> q
p, q:positive

p~0 * q <> q
p, q:positive
IHq:p~0 * q <> q

p~0 * q~0 <> q~0
rewrite mul_xO_r; injection; auto. Qed.

Simplification properties of multiplication

p, q, r:positive

p * r = q * r -> p = q
p, q, r:positive

p * r = q * r -> p = q
p:positive

forall q r : positive, p * r = q * r -> p = q
p:positive
IHp:forall q0 r0 : positive, p * r0 = q0 * r0 -> p = q0
q, r:positive
H:p~1 * r = q~1 * r

p = q
p:positive
IHp:forall q0 r0 : positive, p * r0 = q0 * r0 -> p = q0
q, r:positive
H:p~1 * r = q~0 * r
False
p:positive
IHp:forall q r0 : positive, p * r0 = q * r0 -> p = q
r:positive
H:p~1 * r = 1 * r
False
p:positive
IHp:forall q0 r0 : positive, p * r0 = q0 * r0 -> p = q0
q, r:positive
H:p~0 * r = q~1 * r
False
p:positive
IHp:forall q0 r0 : positive, p * r0 = q0 * r0 -> p = q0
q, r:positive
H:p~0 * r = q~0 * r
p = q
p:positive
IHp:forall q r0 : positive, p * r0 = q * r0 -> p = q
r:positive
H:p~0 * r = 1 * r
False
q, r:positive
H:1 * r = q~1 * r
False
q, r:positive
H:1 * r = q~0 * r
False
p:positive
IHp:forall q0 r0 : positive, p * r0 = q0 * r0 -> p = q0
q, r:positive
H:p~1 * r = q~1 * r

p * r~0 = q * r~0
p:positive
IHp:forall q0 r0 : positive, p * r0 = q0 * r0 -> p = q0
q, r:positive
H:p~1 * r = q~0 * r
False
p:positive
IHp:forall q r0 : positive, p * r0 = q * r0 -> p = q
r:positive
H:p~1 * r = 1 * r
False
p:positive
IHp:forall q0 r0 : positive, p * r0 = q0 * r0 -> p = q0
q, r:positive
H:p~0 * r = q~1 * r
False
p:positive
IHp:forall q0 r0 : positive, p * r0 = q0 * r0 -> p = q0
q, r:positive
H:p~0 * r = q~0 * r
p = q
p:positive
IHp:forall q r0 : positive, p * r0 = q * r0 -> p = q
r:positive
H:p~0 * r = 1 * r
False
q, r:positive
H:1 * r = q~1 * r
False
q, r:positive
H:1 * r = q~0 * r
False
p:positive
IHp:forall q0 r0 : positive, p * r0 = q0 * r0 -> p = q0
q, r:positive
H:r + (p * r)~0 = r + (q * r)~0

p * r~0 = q * r~0
p:positive
IHp:forall q0 r0 : positive, p * r0 = q0 * r0 -> p = q0
q, r:positive
H:p~1 * r = q~0 * r
False
p:positive
IHp:forall q r0 : positive, p * r0 = q * r0 -> p = q
r:positive
H:p~1 * r = 1 * r
False
p:positive
IHp:forall q0 r0 : positive, p * r0 = q0 * r0 -> p = q0
q, r:positive
H:p~0 * r = q~1 * r
False
p:positive
IHp:forall q0 r0 : positive, p * r0 = q0 * r0 -> p = q0
q, r:positive
H:p~0 * r = q~0 * r
p = q
p:positive
IHp:forall q r0 : positive, p * r0 = q * r0 -> p = q
r:positive
H:p~0 * r = 1 * r
False
q, r:positive
H:1 * r = q~1 * r
False
q, r:positive
H:1 * r = q~0 * r
False
p:positive
IHp:forall q0 r0 : positive, p * r0 = q0 * r0 -> p = q0
q, r:positive
H:r + (p * r)~0 = r + (q * r)~0

(p * r)~0 = (q * r)~0
p:positive
IHp:forall q0 r0 : positive, p * r0 = q0 * r0 -> p = q0
q, r:positive
H:p~1 * r = q~0 * r
False
p:positive
IHp:forall q r0 : positive, p * r0 = q * r0 -> p = q
r:positive
H:p~1 * r = 1 * r
False
p:positive
IHp:forall q0 r0 : positive, p * r0 = q0 * r0 -> p = q0
q, r:positive
H:p~0 * r = q~1 * r
False
p:positive
IHp:forall q0 r0 : positive, p * r0 = q0 * r0 -> p = q0
q, r:positive
H:p~0 * r = q~0 * r
p = q
p:positive
IHp:forall q r0 : positive, p * r0 = q * r0 -> p = q
r:positive
H:p~0 * r = 1 * r
False
q, r:positive
H:1 * r = q~1 * r
False
q, r:positive
H:1 * r = q~0 * r
False
p:positive
IHp:forall q0 r0 : positive, p * r0 = q0 * r0 -> p = q0
q, r:positive
H:p~1 * r = q~0 * r

False
p:positive
IHp:forall q r0 : positive, p * r0 = q * r0 -> p = q
r:positive
H:p~1 * r = 1 * r
False
p:positive
IHp:forall q0 r0 : positive, p * r0 = q0 * r0 -> p = q0
q, r:positive
H:p~0 * r = q~1 * r
False
p:positive
IHp:forall q0 r0 : positive, p * r0 = q0 * r0 -> p = q0
q, r:positive
H:p~0 * r = q~0 * r
p = q
p:positive
IHp:forall q r0 : positive, p * r0 = q * r0 -> p = q
r:positive
H:p~0 * r = 1 * r
False
q, r:positive
H:1 * r = q~1 * r
False
q, r:positive
H:1 * r = q~0 * r
False
p:positive
IHp:forall q0 r0 : positive, p * r0 = q0 * r0 -> p = q0
q, r:positive

p~1 * r <> q~0 * r
p:positive
IHp:forall q r0 : positive, p * r0 = q * r0 -> p = q
r:positive
H:p~1 * r = 1 * r
False
p:positive
IHp:forall q0 r0 : positive, p * r0 = q0 * r0 -> p = q0
q, r:positive
H:p~0 * r = q~1 * r
False
p:positive
IHp:forall q0 r0 : positive, p * r0 = q0 * r0 -> p = q0
q, r:positive
H:p~0 * r = q~0 * r
p = q
p:positive
IHp:forall q r0 : positive, p * r0 = q * r0 -> p = q
r:positive
H:p~0 * r = 1 * r
False
q, r:positive
H:1 * r = q~1 * r
False
q, r:positive
H:1 * r = q~0 * r
False
p:positive
IHp:forall q r0 : positive, p * r0 = q * r0 -> p = q
r:positive
H:p~1 * r = 1 * r

False
p:positive
IHp:forall q0 r0 : positive, p * r0 = q0 * r0 -> p = q0
q, r:positive
H:p~0 * r = q~1 * r
False
p:positive
IHp:forall q0 r0 : positive, p * r0 = q0 * r0 -> p = q0
q, r:positive
H:p~0 * r = q~0 * r
p = q
p:positive
IHp:forall q r0 : positive, p * r0 = q * r0 -> p = q
r:positive
H:p~0 * r = 1 * r
False
q, r:positive
H:1 * r = q~1 * r
False
q, r:positive
H:1 * r = q~0 * r
False
p:positive
IHp:forall q r0 : positive, p * r0 = q * r0 -> p = q
r:positive

p~1 * r <> 1 * r
p:positive
IHp:forall q0 r0 : positive, p * r0 = q0 * r0 -> p = q0
q, r:positive
H:p~0 * r = q~1 * r
False
p:positive
IHp:forall q0 r0 : positive, p * r0 = q0 * r0 -> p = q0
q, r:positive
H:p~0 * r = q~0 * r
p = q
p:positive
IHp:forall q r0 : positive, p * r0 = q * r0 -> p = q
r:positive
H:p~0 * r = 1 * r
False
q, r:positive
H:1 * r = q~1 * r
False
q, r:positive
H:1 * r = q~0 * r
False
p:positive
IHp:forall q r0 : positive, p * r0 = q * r0 -> p = q
r:positive

r + (p * r)~0 <> r
p:positive
IHp:forall q0 r0 : positive, p * r0 = q0 * r0 -> p = q0
q, r:positive
H:p~0 * r = q~1 * r
False
p:positive
IHp:forall q0 r0 : positive, p * r0 = q0 * r0 -> p = q0
q, r:positive
H:p~0 * r = q~0 * r
p = q
p:positive
IHp:forall q r0 : positive, p * r0 = q * r0 -> p = q
r:positive
H:p~0 * r = 1 * r
False
q, r:positive
H:1 * r = q~1 * r
False
q, r:positive
H:1 * r = q~0 * r
False
p:positive
IHp:forall q r0 : positive, p * r0 = q * r0 -> p = q
r:positive

(p * r)~0 + r <> r
p:positive
IHp:forall q0 r0 : positive, p * r0 = q0 * r0 -> p = q0
q, r:positive
H:p~0 * r = q~1 * r
False
p:positive
IHp:forall q0 r0 : positive, p * r0 = q0 * r0 -> p = q0
q, r:positive
H:p~0 * r = q~0 * r
p = q
p:positive
IHp:forall q r0 : positive, p * r0 = q * r0 -> p = q
r:positive
H:p~0 * r = 1 * r
False
q, r:positive
H:1 * r = q~1 * r
False
q, r:positive
H:1 * r = q~0 * r
False
p:positive
IHp:forall q0 r0 : positive, p * r0 = q0 * r0 -> p = q0
q, r:positive
H:p~0 * r = q~1 * r

False
p:positive
IHp:forall q0 r0 : positive, p * r0 = q0 * r0 -> p = q0
q, r:positive
H:p~0 * r = q~0 * r
p = q
p:positive
IHp:forall q r0 : positive, p * r0 = q * r0 -> p = q
r:positive
H:p~0 * r = 1 * r
False
q, r:positive
H:1 * r = q~1 * r
False
q, r:positive
H:1 * r = q~0 * r
False
p:positive
IHp:forall q0 r0 : positive, p * r0 = q0 * r0 -> p = q0
q, r:positive
H:q~1 * r = p~0 * r

False
p:positive
IHp:forall q0 r0 : positive, p * r0 = q0 * r0 -> p = q0
q, r:positive
H:p~0 * r = q~0 * r
p = q
p:positive
IHp:forall q r0 : positive, p * r0 = q * r0 -> p = q
r:positive
H:p~0 * r = 1 * r
False
q, r:positive
H:1 * r = q~1 * r
False
q, r:positive
H:1 * r = q~0 * r
False
p:positive
IHp:forall q0 r0 : positive, p * r0 = q0 * r0 -> p = q0
q, r:positive

q~1 * r <> p~0 * r
p:positive
IHp:forall q0 r0 : positive, p * r0 = q0 * r0 -> p = q0
q, r:positive
H:p~0 * r = q~0 * r
p = q
p:positive
IHp:forall q r0 : positive, p * r0 = q * r0 -> p = q
r:positive
H:p~0 * r = 1 * r
False
q, r:positive
H:1 * r = q~1 * r
False
q, r:positive
H:1 * r = q~0 * r
False
p:positive
IHp:forall q0 r0 : positive, p * r0 = q0 * r0 -> p = q0
q, r:positive
H:p~0 * r = q~0 * r

p = q
p:positive
IHp:forall q r0 : positive, p * r0 = q * r0 -> p = q
r:positive
H:p~0 * r = 1 * r
False
q, r:positive
H:1 * r = q~1 * r
False
q, r:positive
H:1 * r = q~0 * r
False
p:positive
IHp:forall q0 r0 : positive, p * r0 = q0 * r0 -> p = q0
q, r:positive
H:p~0 * r = q~0 * r

p * r~0 = q * r~0
p:positive
IHp:forall q r0 : positive, p * r0 = q * r0 -> p = q
r:positive
H:p~0 * r = 1 * r
False
q, r:positive
H:1 * r = q~1 * r
False
q, r:positive
H:1 * r = q~0 * r
False
p:positive
IHp:forall q0 r0 : positive, p * r0 = q0 * r0 -> p = q0
q, r:positive
H:p~0 * r = q~0 * r

p * r~0 = q * r~0
p:positive
IHp:forall q r0 : positive, p * r0 = q * r0 -> p = q
r:positive
H:p~0 * r = 1 * r
False
q, r:positive
H:1 * r = q~1 * r
False
q, r:positive
H:1 * r = q~0 * r
False
p:positive
IHp:forall q r0 : positive, p * r0 = q * r0 -> p = q
r:positive
H:p~0 * r = 1 * r

False
q, r:positive
H:1 * r = q~1 * r
False
q, r:positive
H:1 * r = q~0 * r
False
p:positive
IHp:forall q r0 : positive, p * r0 = q * r0 -> p = q
r:positive

p~0 * r <> 1 * r
q, r:positive
H:1 * r = q~1 * r
False
q, r:positive
H:1 * r = q~0 * r
False
q, r:positive
H:1 * r = q~1 * r

False
q, r:positive
H:1 * r = q~0 * r
False
q, r:positive
H:q~1 * r = 1 * r

False
q, r:positive
H:1 * r = q~0 * r
False
q, r:positive

q~1 * r <> 1 * r
q, r:positive
H:1 * r = q~0 * r
False
q, r:positive

r + (q * r)~0 <> r
q, r:positive
H:1 * r = q~0 * r
False
q, r:positive

(q * r)~0 + r <> r
q, r:positive
H:1 * r = q~0 * r
False
q, r:positive
H:1 * r = q~0 * r

False
q, r:positive
H:q~0 * r = 1 * r

False
q, r:positive

q~0 * r <> 1 * r
apply mul_xO_discr. Qed.
p, q, r:positive

r * p = r * q -> p = q
p, q, r:positive

r * p = r * q -> p = q
p, q, r:positive

p * r = q * r -> p = q
apply mul_reg_r. Qed.
p, q, r:positive

p * r = q * r <-> p = q
p, q, r:positive

p * r = q * r <-> p = q
p, q, r:positive

p * r = q * r -> p = q
p, q, r:positive
p = q -> p * r = q * r
p, q, r:positive

p = q -> p * r = q * r
congruence. Qed.
p, q, r:positive

r * p = r * q <-> p = q
p, q, r:positive

r * p = r * q <-> p = q
p, q, r:positive

r * p = r * q -> p = q
p, q, r:positive
p = q -> r * p = r * q
p, q, r:positive

p = q -> r * p = r * q
congruence. Qed.

Inversion of multiplication

p, q:positive

p * q = 1 -> p = 1
p, q:positive

p * q = 1 -> p = 1
now destruct p, q. Qed.
p, q:positive

p * q = 1 -> q = 1
p, q:positive

p * q = 1 -> q = 1
now destruct p, q. Qed. Notation mul_eq_1 := mul_eq_1_l.

Square

p:positive

p~0 * p~0 = (p * p)~0~0
p:positive

p~0 * p~0 = (p * p)~0~0
p:positive

(p * p~0)~0 = (p * p)~0~0
now rewrite mul_comm. Qed.
p:positive

p~1 * p~1 = (p * p + p)~0~1
p:positive

p~1 * p~1 = (p * p + p)~0~1
p:positive

(p + p * p~1)~1 = (p * p + p)~0~1
p:positive

(p + p~1 * p)~1 = (p * p + p)~0~1
p:positive

(p + (p + (p * p)~0))~1 = (p * p + p)~0~1
p:positive

p + (p + (p * p)~0) = (p * p + p)~0
p:positive

p~0 + (p * p)~0 = (p * p + p)~0
p:positive

(p + p * p)~0 = (p * p + p)~0
now rewrite add_comm. Qed.

Properties of iter


forall (A B : Type) (f : A -> B) (g : A -> A) (h : B -> B), (forall a : A, f (g a) = h (f a)) -> forall (p : positive) (a : A), f (iter g a p) = iter h (f a) p

forall (A B : Type) (f : A -> B) (g : A -> A) (h : B -> B), (forall a : A, f (g a) = h (f a)) -> forall (p : positive) (a : A), f (iter g a p) = iter h (f a) p
induction p; simpl; intros; now rewrite ?H, ?IHp. Qed.

forall (p : positive) (A : Type) (f : A -> A) (x : A), iter f (f x) p = f (iter f x p)

forall (p : positive) (A : Type) (f : A -> A) (x : A), iter f (f x) p = f (iter f x p)
p:positive
A:Type
f:A -> A
x:A

iter f (f x) p = f (iter f x p)
p:positive
A:Type
f:A -> A
x:A

f (iter f x p) = iter f (f x) p
now apply iter_swap_gen. Qed.

forall (p : positive) (A : Type) (f : A -> A) (x : A), iter f x (succ p) = f (iter f x p)

forall (p : positive) (A : Type) (f : A -> A) (x : A), iter f x (succ p) = f (iter f x p)
p:positive
IHp:forall (A0 : Type) (f0 : A0 -> A0) (x0 : A0), iter f0 x0 (succ p) = f0 (iter f0 x0 p)
A:Type
f:A -> A
x:A

iter f (iter f x (succ p)) (succ p) = f (f (iter f (iter f x p) p))
now rewrite !IHp, iter_swap. Qed.

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

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

iter f x (1 + q) = iter f (iter f x q) 1
p:positive
IHp:forall (q0 : positive) (A0 : Type) (f0 : A0 -> A0) (x0 : A0), iter f0 x0 (p + q0) = iter f0 (iter f0 x0 q0) p
q:positive
A:Type
f:A -> A
x:A
iter f x (succ p + q) = iter f (iter f x q) (succ p)
p:positive
IHp:forall (q0 : positive) (A0 : Type) (f0 : A0 -> A0) (x0 : A0), iter f0 x0 (p + q0) = iter f0 (iter f0 x0 q0) p
q:positive
A:Type
f:A -> A
x:A

iter f x (succ p + q) = iter f (iter f x q) (succ p)
now rewrite add_succ_l, !iter_succ, IHp. Qed.

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 f x p)

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 f x p)
p:positive
IHp:forall (A : Type) (f : A -> A) (Inv : A -> Prop), (forall x : A, Inv x -> Inv (f x)) -> forall x : A, Inv x -> Inv (iter f x p)

forall (A : Type) (f : A -> A) (Inv : A -> Prop), (forall x : A, Inv x -> Inv (f x)) -> forall x : A, Inv x -> Inv (f (iter f (iter f x p) p))
p:positive
IHp:forall (A : Type) (f : A -> A) (Inv : A -> Prop), (forall x : A, Inv x -> Inv (f x)) -> forall x : A, Inv x -> Inv (iter f x p)
forall (A : Type) (f : A -> A) (Inv : A -> Prop), (forall x : A, Inv x -> Inv (f x)) -> forall x : A, Inv x -> Inv (iter f (iter f x p) p)
p:positive
IHp:forall (A0 : Type) (f0 : A0 -> A0) (Inv0 : A0 -> Prop), (forall x0 : A0, Inv0 x0 -> Inv0 (f0 x0)) -> forall x0 : A0, Inv0 x0 -> Inv0 (iter f0 x0 p)
A:Type
f:A -> A
Inv:A -> Prop
H:forall x0 : A, Inv x0 -> Inv (f x0)
x:A
H0:Inv x

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

forall (A : Type) (f : A -> A) (Inv : A -> Prop), (forall x : A, Inv x -> Inv (f x)) -> forall x : A, Inv x -> Inv (iter f (iter f x p) p)
p:positive
IHp:forall (A0 : Type) (f0 : A0 -> A0) (Inv0 : A0 -> Prop), (forall x0 : A0, Inv0 x0 -> Inv0 (f0 x0)) -> forall x0 : A0, Inv0 x0 -> Inv0 (iter f0 x0 p)
A:Type
f:A -> A
Inv:A -> Prop
H:forall x0 : A, Inv x0 -> Inv (f x0)
x:A
H0:Inv x

Inv (iter f (iter f x p) p)
apply IHp, IHp; trivial. Qed.

Properties of power

p:positive

p ^ 1 = p
p:positive

p ^ 1 = p
p:positive

iter (mul p) 1 1 = p
p:positive

p * 1 = p
now rewrite mul_comm. Qed.
p, q:positive

p ^ succ q = p * p ^ q
p, q:positive

p ^ succ q = p * p ^ q
p, q:positive

iter (mul p) 1 (succ q) = p * iter (mul p) 1 q
now rewrite iter_succ. Qed.

Properties of square

p:positive

square p = p * p
p:positive

square p = p * p
p:positive
IHp:square p = p * p

square p~1 = p~1 * p~1
p:positive
IHp:square p = p * p
square p~0 = p~0 * p~0

square 1 = 1 * 1
p:positive
IHp:square p = p * p

square p~1 = p~1 * p~1
p:positive
IHp:square p = p * p

square p~1 = (p * p + p)~0~1
p:positive
IHp:square p = p * p

(square p + p)~0~1 = (p * p + p)~0~1
now rewrite IHp.
p:positive
IHp:square p = p * p

square p~0 = p~0 * p~0
p:positive
IHp:square p = p * p

square p~0 = (p * p)~0~0
p:positive
IHp:square p = p * p

(square p)~0~0 = (p * p)~0~0
now rewrite IHp.

square 1 = 1 * 1
trivial. Qed.

Properties of sub_mask

p, q:positive

sub_mask p (succ q) = sub_mask_carry p q
p, q:positive

sub_mask p (succ q) = sub_mask_carry p q
p:positive

forall q : positive, sub_mask p (succ q) = sub_mask_carry p q
induction p; destruct q; simpl; f_equal; trivial; now destruct p. Qed.
p, q:positive

sub_mask_carry p q = pred_mask (sub_mask p q)
p, q:positive

sub_mask_carry p q = pred_mask (sub_mask p q)
p:positive

forall q : positive, sub_mask_carry p q = pred_mask (sub_mask p q)
induction p as [p IHp|p IHp| ]; destruct q; simpl; try reflexivity; rewrite ?IHp; destruct (sub_mask p q) as [|[r|r| ]|] || destruct p; auto. Qed. 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.
p, q:positive

SubMaskSpec p q (sub_mask p q)
p, q:positive

SubMaskSpec p q (sub_mask p q)
p:positive

forall q : positive, SubMaskSpec p q (sub_mask p q)
p:positive
IHp:forall q0 : positive, SubMaskSpec p q0 (sub_mask p q0)
q:positive

SubMaskSpec p~1 q~1 (double_mask (sub_mask p q))
p:positive
IHp:forall q0 : positive, SubMaskSpec p q0 (sub_mask p q0)
q:positive
SubMaskSpec p~1 q~0 (succ_double_mask (sub_mask p q))
p:positive
IHp:forall q0 : positive, SubMaskSpec p q0 (sub_mask p q0)
q:positive
SubMaskSpec p~0 q~1 (succ_double_mask (sub_mask_carry p q))
p:positive
IHp:forall q0 : positive, SubMaskSpec p q0 (sub_mask p q0)
q:positive
SubMaskSpec p~0 q~0 (double_mask (sub_mask p q))
p:positive
IHp:forall q : positive, SubMaskSpec p q (sub_mask p q)
1 + pred_double p = p~0
q:positive
SubMaskSpec 1 q~1 IsNeg
q:positive
SubMaskSpec 1 q~0 IsNeg
(* p~1 q~1 *)
p:positive
IHp:forall q : positive, SubMaskSpec p q (sub_mask p q)
r:positive

SubMaskSpec p~1 (p + r)~1 (double_mask IsNeg)
p:positive
IHp:forall q0 : positive, SubMaskSpec p q0 (sub_mask p q0)
q:positive
SubMaskSpec p~1 q~0 (succ_double_mask (sub_mask p q))
p:positive
IHp:forall q0 : positive, SubMaskSpec p q0 (sub_mask p q0)
q:positive
SubMaskSpec p~0 q~1 (succ_double_mask (sub_mask_carry p q))
p:positive
IHp:forall q0 : positive, SubMaskSpec p q0 (sub_mask p q0)
q:positive
SubMaskSpec p~0 q~0 (double_mask (sub_mask p q))
p:positive
IHp:forall q : positive, SubMaskSpec p q (sub_mask p q)
1 + pred_double p = p~0
q:positive
SubMaskSpec 1 q~1 IsNeg
q:positive
SubMaskSpec 1 q~0 IsNeg
p:positive
IHp:forall q0 : positive, SubMaskSpec p q0 (sub_mask p q0)
q:positive

SubMaskSpec p~1 q~0 (succ_double_mask (sub_mask p q))
p:positive
IHp:forall q0 : positive, SubMaskSpec p q0 (sub_mask p q0)
q:positive
SubMaskSpec p~0 q~1 (succ_double_mask (sub_mask_carry p q))
p:positive
IHp:forall q0 : positive, SubMaskSpec p q0 (sub_mask p q0)
q:positive
SubMaskSpec p~0 q~0 (double_mask (sub_mask p q))
p:positive
IHp:forall q : positive, SubMaskSpec p q (sub_mask p q)
1 + pred_double p = p~0
q:positive
SubMaskSpec 1 q~1 IsNeg
q:positive
SubMaskSpec 1 q~0 IsNeg
(* p~1 q~0 *)
p:positive
IHp:forall q : positive, SubMaskSpec p q (sub_mask p q)
r:positive

SubMaskSpec p~1 (p + r)~0 (succ_double_mask IsNeg)
p:positive
IHp:forall q0 : positive, SubMaskSpec p q0 (sub_mask p q0)
q:positive
SubMaskSpec p~0 q~1 (succ_double_mask (sub_mask_carry p q))
p:positive
IHp:forall q0 : positive, SubMaskSpec p q0 (sub_mask p q0)
q:positive
SubMaskSpec p~0 q~0 (double_mask (sub_mask p q))
p:positive
IHp:forall q : positive, SubMaskSpec p q (sub_mask p q)
1 + pred_double p = p~0
q:positive
SubMaskSpec 1 q~1 IsNeg
q:positive
SubMaskSpec 1 q~0 IsNeg
p:positive
IHp:forall q : positive, SubMaskSpec p q (sub_mask p q)
r:positive

p~1 + pred_double r = (p + r)~0
p:positive
IHp:forall q0 : positive, SubMaskSpec p q0 (sub_mask p q0)
q:positive
SubMaskSpec p~0 q~1 (succ_double_mask (sub_mask_carry p q))
p:positive
IHp:forall q0 : positive, SubMaskSpec p q0 (sub_mask p q0)
q:positive
SubMaskSpec p~0 q~0 (double_mask (sub_mask p q))
p:positive
IHp:forall q : positive, SubMaskSpec p q (sub_mask p q)
1 + pred_double p = p~0
q:positive
SubMaskSpec 1 q~1 IsNeg
q:positive
SubMaskSpec 1 q~0 IsNeg
p:positive
IHp:forall q : positive, SubMaskSpec p q (sub_mask p q)
r:positive

(p + r)~0 = p~1 + pred_double r
p:positive
IHp:forall q0 : positive, SubMaskSpec p q0 (sub_mask p q0)
q:positive
SubMaskSpec p~0 q~1 (succ_double_mask (sub_mask_carry p q))
p:positive
IHp:forall q0 : positive, SubMaskSpec p q0 (sub_mask p q0)
q:positive
SubMaskSpec p~0 q~0 (double_mask (sub_mask p q))
p:positive
IHp:forall q : positive, SubMaskSpec p q (sub_mask p q)
1 + pred_double p = p~0
q:positive
SubMaskSpec 1 q~1 IsNeg
q:positive
SubMaskSpec 1 q~0 IsNeg
p:positive
IHp:forall q0 : positive, SubMaskSpec p q0 (sub_mask p q0)
q:positive

SubMaskSpec p~0 q~1 (succ_double_mask (sub_mask_carry p q))
p:positive
IHp:forall q0 : positive, SubMaskSpec p q0 (sub_mask p q0)
q:positive
SubMaskSpec p~0 q~0 (double_mask (sub_mask p q))
p:positive
IHp:forall q : positive, SubMaskSpec p q (sub_mask p q)
1 + pred_double p = p~0
q:positive
SubMaskSpec 1 q~1 IsNeg
q:positive
SubMaskSpec 1 q~0 IsNeg
(* p~0 q~1 *)
p:positive
IHp:forall q0 : positive, SubMaskSpec p q0 (sub_mask p q0)
q:positive

SubMaskSpec p~0 q~1 (succ_double_mask (pred_mask (sub_mask p q)))
p:positive
IHp:forall q0 : positive, SubMaskSpec p q0 (sub_mask p q0)
q:positive
SubMaskSpec p~0 q~0 (double_mask (sub_mask p q))
p:positive
IHp:forall q : positive, SubMaskSpec p q (sub_mask p q)
1 + pred_double p = p~0
q:positive
SubMaskSpec 1 q~1 IsNeg
q:positive
SubMaskSpec 1 q~0 IsNeg
q:positive
IHp:forall q0 : positive, SubMaskSpec q q0 (sub_mask q q0)

SubMaskSpec q~0 q~1 (succ_double_mask (pred_mask IsNul))
q, r:positive
IHp:forall q0 : positive, SubMaskSpec (q + r) q0 (sub_mask (q + r) q0)
SubMaskSpec (q + r)~0 q~1 (succ_double_mask (pred_mask (IsPos r)))
p:positive
IHp:forall q : positive, SubMaskSpec p q (sub_mask p q)
r:positive
SubMaskSpec p~0 (p + r)~1 (succ_double_mask (pred_mask IsNeg))
p:positive
IHp:forall q0 : positive, SubMaskSpec p q0 (sub_mask p q0)
q:positive
SubMaskSpec p~0 q~0 (double_mask (sub_mask p q))
p:positive
IHp:forall q : positive, SubMaskSpec p q (sub_mask p q)
1 + pred_double p = p~0
q:positive
SubMaskSpec 1 q~1 IsNeg
q:positive
SubMaskSpec 1 q~0 IsNeg
q, r:positive
IHp:forall q0 : positive, SubMaskSpec (q + r) q0 (sub_mask (q + r) q0)

SubMaskSpec (q + r)~0 q~1 (succ_double_mask (pred_mask (IsPos r)))
p:positive
IHp:forall q : positive, SubMaskSpec p q (sub_mask p q)
r:positive
SubMaskSpec p~0 (p + r)~1 (succ_double_mask (pred_mask IsNeg))
p:positive
IHp:forall q0 : positive, SubMaskSpec p q0 (sub_mask p q0)
q:positive
SubMaskSpec p~0 q~0 (double_mask (sub_mask p q))
p:positive
IHp:forall q : positive, SubMaskSpec p q (sub_mask p q)
1 + pred_double p = p~0
q:positive
SubMaskSpec 1 q~1 IsNeg
q:positive
SubMaskSpec 1 q~0 IsNeg
q, r:positive
IHp:forall q0 : positive, SubMaskSpec (q + r~1) q0 (sub_mask (q + r~1) q0)

(add_carry q r~0)~0 = (q + r~1)~0
q, r:positive
IHp:forall q0 : positive, SubMaskSpec (q + r~0) q0 (sub_mask (q + r~0) q0)
(add_carry q (pred_double r))~0 = (q + r~0)~0
q:positive
IHp:forall q0 : positive, SubMaskSpec (q + 1) q0 (sub_mask (q + 1) q0)
(succ q)~0 = (q + 1)~0
p:positive
IHp:forall q : positive, SubMaskSpec p q (sub_mask p q)
r:positive
SubMaskSpec p~0 (p + r)~1 (succ_double_mask (pred_mask IsNeg))
p:positive
IHp:forall q0 : positive, SubMaskSpec p q0 (sub_mask p q0)
q:positive
SubMaskSpec p~0 q~0 (double_mask (sub_mask p q))
p:positive
IHp:forall q : positive, SubMaskSpec p q (sub_mask p q)
1 + pred_double p = p~0
q:positive
SubMaskSpec 1 q~1 IsNeg
q:positive
SubMaskSpec 1 q~0 IsNeg
q, r:positive
IHp:forall q0 : positive, SubMaskSpec (q + r~0) q0 (sub_mask (q + r~0) q0)

(add_carry q (pred_double r))~0 = (q + r~0)~0
q:positive
IHp:forall q0 : positive, SubMaskSpec (q + 1) q0 (sub_mask (q + 1) q0)
(succ q)~0 = (q + 1)~0
p:positive
IHp:forall q : positive, SubMaskSpec p q (sub_mask p q)
r:positive
SubMaskSpec p~0 (p + r)~1 (succ_double_mask (pred_mask IsNeg))
p:positive
IHp:forall q0 : positive, SubMaskSpec p q0 (sub_mask p q0)
q:positive
SubMaskSpec p~0 q~0 (double_mask (sub_mask p q))
p:positive
IHp:forall q : positive, SubMaskSpec p q (sub_mask p q)
1 + pred_double p = p~0
q:positive
SubMaskSpec 1 q~1 IsNeg
q:positive
SubMaskSpec 1 q~0 IsNeg
q:positive
IHp:forall q0 : positive, SubMaskSpec (q + 1) q0 (sub_mask (q + 1) q0)

(succ q)~0 = (q + 1)~0
p:positive
IHp:forall q : positive, SubMaskSpec p q (sub_mask p q)
r:positive
SubMaskSpec p~0 (p + r)~1 (succ_double_mask (pred_mask IsNeg))
p:positive
IHp:forall q0 : positive, SubMaskSpec p q0 (sub_mask p q0)
q:positive
SubMaskSpec p~0 q~0 (double_mask (sub_mask p q))
p:positive
IHp:forall q : positive, SubMaskSpec p q (sub_mask p q)
1 + pred_double p = p~0
q:positive
SubMaskSpec 1 q~1 IsNeg
q:positive
SubMaskSpec 1 q~0 IsNeg
p:positive
IHp:forall q : positive, SubMaskSpec p q (sub_mask p q)
r:positive

SubMaskSpec p~0 (p + r)~1 (succ_double_mask (pred_mask IsNeg))
p:positive
IHp:forall q0 : positive, SubMaskSpec p q0 (sub_mask p q0)
q:positive
SubMaskSpec p~0 q~0 (double_mask (sub_mask p q))
p:positive
IHp:forall q : positive, SubMaskSpec p q (sub_mask p q)
1 + pred_double p = p~0
q:positive
SubMaskSpec 1 q~1 IsNeg
q:positive
SubMaskSpec 1 q~0 IsNeg
p:positive
IHp:forall q0 : positive, SubMaskSpec p q0 (sub_mask p q0)
q:positive

SubMaskSpec p~0 q~0 (double_mask (sub_mask p q))
p:positive
IHp:forall q : positive, SubMaskSpec p q (sub_mask p q)
1 + pred_double p = p~0
q:positive
SubMaskSpec 1 q~1 IsNeg
q:positive
SubMaskSpec 1 q~0 IsNeg
(* p~0 q~0 *)
p:positive
IHp:forall q : positive, SubMaskSpec p q (sub_mask p q)
r:positive

SubMaskSpec p~0 (p + r)~0 (double_mask IsNeg)
p:positive
IHp:forall q : positive, SubMaskSpec p q (sub_mask p q)
1 + pred_double p = p~0
q:positive
SubMaskSpec 1 q~1 IsNeg
q:positive
SubMaskSpec 1 q~0 IsNeg
p:positive
IHp:forall q : positive, SubMaskSpec p q (sub_mask p q)

1 + pred_double p = p~0
q:positive
SubMaskSpec 1 q~1 IsNeg
q:positive
SubMaskSpec 1 q~0 IsNeg
(* p~0 1 *)
q:positive

SubMaskSpec 1 q~1 IsNeg
q:positive
SubMaskSpec 1 q~0 IsNeg
(* 1 q~1 *)
q:positive

SubMaskSpec 1 q~0 IsNeg
(* 1 q~0 *)
q:positive

1 + pred_double q = q~0
now rewrite add_1_l, succ_pred_double. Qed.
p, q:positive

sub_mask p q = IsNul <-> p = q
p, q:positive

sub_mask p q = IsNul <-> p = q
p, q:positive

sub_mask p q = IsNul -> p = q
p, q:positive
p = q -> sub_mask p q = IsNul
p, q:positive

p = q -> sub_mask p q = IsNul
p:positive

sub_mask p p = IsNul
induction p; simpl; now rewrite ?IHp. Qed.
p:positive

sub_mask p p = IsNul
p:positive

sub_mask p p = IsNul
now apply sub_mask_nul_iff. Qed.
p, q, r:positive

sub_mask p q = IsPos r -> q + r = p
p, q, r:positive

sub_mask p q = IsPos r -> q + r = p
case sub_mask_spec; congruence. Qed.
p, q:positive

sub_mask (p + q) p = IsPos q
p, q:positive

sub_mask (p + q) p = IsPos q
p, q:positive

p + q = p -> IsNul = IsPos q
p, q:positive
forall r : positive, p + r = p + q -> IsPos r = IsPos q
p, q:positive
forall r : positive, p + q + r = p -> IsNeg = IsPos q
p, q:positive
H:p + q = p

IsNul = IsPos q
p, q:positive
forall r : positive, p + r = p + q -> IsPos r = IsPos q
p, q:positive
forall r : positive, p + q + r = p -> IsNeg = IsPos q
p, q:positive
H:q + p = p

IsNul = IsPos q
p, q:positive
forall r : positive, p + r = p + q -> IsPos r = IsPos q
p, q:positive
forall r : positive, p + q + r = p -> IsNeg = IsPos q
p, q:positive

forall r : positive, p + r = p + q -> IsPos r = IsPos q
p, q:positive
forall r : positive, p + q + r = p -> IsNeg = IsPos q
p, q, r:positive
H:p + r = p + q

IsPos r = IsPos q
p, q:positive
forall r : positive, p + q + r = p -> IsNeg = IsPos q
p, q, r:positive
H:r = q

IsPos r = IsPos q
p, q:positive
forall r : positive, p + q + r = p -> IsNeg = IsPos q
p, q:positive

forall r : positive, p + q + r = p -> IsNeg = IsPos q
p, q, r:positive
H:p + q + r = p

IsNeg = IsPos q
p, q, r:positive
H:q + r + p = p

IsNeg = IsPos q
elim (add_no_neutral _ _ H). Qed.
p, q, r:positive

sub_mask p q = IsPos r <-> q + r = p
p, q, r:positive

sub_mask p q = IsPos r <-> q + r = p
p, q, r:positive

sub_mask p q = IsPos r -> q + r = p
p, q, r:positive
q + r = p -> sub_mask p q = IsPos r
p, q, r:positive

q + r = p -> sub_mask p q = IsPos r
intros <-; apply sub_mask_add_diag_l. Qed.
p, q:positive

sub_mask p (p + q) = IsNeg
p, q:positive

sub_mask p (p + q) = IsNeg
p, q:positive

p = p + q -> IsNul = IsNeg
p, q:positive
forall r : positive, p + q + r = p -> IsPos r = IsNeg
p, q:positive
H:p = p + q

IsNul = IsNeg
p, q:positive
forall r : positive, p + q + r = p -> IsPos r = IsNeg
p, q:positive
H:q + p = p

IsNul = IsNeg
p, q:positive
forall r : positive, p + q + r = p -> IsPos r = IsNeg
p, q:positive

forall r : positive, p + q + r = p -> IsPos r = IsNeg
p, q, r:positive
H:p + q + r = p

IsPos r = IsNeg
p, q, r:positive
H:q + r + p = p

IsPos r = IsNeg
elim (add_no_neutral _ _ H). Qed.
p, q:positive

sub_mask p q = IsNeg <-> (exists r : positive, p + r = q)
p, q:positive

sub_mask p q = IsNeg <-> (exists r : positive, p + r = q)
p, q:positive

sub_mask p q = IsNeg -> exists r : positive, p + r = q
p, q:positive
(exists r : positive, p + r = q) -> sub_mask p q = IsNeg
p, q:positive

forall r : positive, p + r = q -> IsNeg = IsNeg -> exists r0 : positive, p + r0 = q
p, q:positive
(exists r : positive, p + r = q) -> sub_mask p q = IsNeg
p, q:positive

(exists r : positive, p + r = q) -> sub_mask p q = IsNeg
p, r:positive

sub_mask p (p + r) = IsNeg
apply sub_mask_add_diag_r. Qed. (*********************************************************************)

Properties of boolean comparisons

p, q:positive

(p =? q) = true <-> p = q
p, q:positive

(p =? q) = true <-> p = q
p:positive

forall q : positive, (p =? q) = true <-> p = q
induction p; destruct q; simpl; rewrite ?IHp; split; congruence. Qed.
p, q:positive

(p <? q) = true <-> p < q
p, q:positive

(p <? q) = true <-> p < q
p, q:positive

match p ?= q with | Lt => true | _ => false end = true <-> (p ?= q) = Lt
destruct compare; easy'. Qed.
p, q:positive

(p <=? q) = true <-> p <= q
p, q:positive

(p <=? q) = true <-> p <= q
p, q:positive

match p ?= q with | Gt => false | _ => true end = true <-> (p ?= q) <> Gt
destruct compare; easy'. Qed.
More about eqb
Include BoolEqualityFacts.

(**********************************************************************)

Properties of comparison on binary positive numbers

First, we express compare_cont in term of compare
Definition switch_Eq c c' :=
 match c' with
  | Eq => c
  | Lt => Lt
  | Gt => Gt
 end.

p, q:positive
c:comparison

compare_cont c p q = switch_Eq c (p ?= q)
p, q:positive
c:comparison

compare_cont c p q = switch_Eq c (p ?= q)
p, q:positive
c:comparison

compare_cont c p q = switch_Eq c (compare_cont Eq p q)
p:positive

forall (q : positive) (c : comparison), compare_cont c p q = switch_Eq c (compare_cont Eq p q)
p:positive
IHp:forall (q0 : positive) (c : comparison), compare_cont c p q0 = switch_Eq c (compare_cont Eq p q0)
q:positive

forall c : comparison, compare_cont Gt p q = switch_Eq c (compare_cont Gt p q)
p:positive
IHp:forall (q0 : positive) (c : comparison), compare_cont c p q0 = switch_Eq c (compare_cont Eq p q0)
q:positive
forall c : comparison, compare_cont Lt p q = switch_Eq c (compare_cont Lt p q)
p:positive
IHp:forall (q0 : positive) (c0 : comparison), compare_cont c0 p q0 = switch_Eq c0 (compare_cont Eq p q0)
q:positive
c:comparison

compare_cont Gt p q = switch_Eq c (compare_cont Gt p q)
p:positive
IHp:forall (q0 : positive) (c : comparison), compare_cont c p q0 = switch_Eq c (compare_cont Eq p q0)
q:positive
forall c : comparison, compare_cont Lt p q = switch_Eq c (compare_cont Lt p q)
p:positive
IHp:forall (q0 : positive) (c0 : comparison), compare_cont c0 p q0 = switch_Eq c0 (compare_cont Eq p q0)
q:positive
c:comparison

switch_Eq Gt (switch_Eq Eq (compare_cont Eq p q)) = switch_Eq c (switch_Eq Gt (switch_Eq Eq (compare_cont Eq p q)))
p:positive
IHp:forall (q0 : positive) (c : comparison), compare_cont c p q0 = switch_Eq c (compare_cont Eq p q0)
q:positive
forall c : comparison, compare_cont Lt p q = switch_Eq c (compare_cont Lt p q)
p:positive
IHp:forall (q0 : positive) (c : comparison), compare_cont c p q0 = switch_Eq c (compare_cont Eq p q0)
q:positive

forall c : comparison, compare_cont Lt p q = switch_Eq c (compare_cont Lt p q)
p:positive
IHp:forall (q0 : positive) (c0 : comparison), compare_cont c0 p q0 = switch_Eq c0 (compare_cont Eq p q0)
q:positive
c:comparison

compare_cont Lt p q = switch_Eq c (compare_cont Lt p q)
p:positive
IHp:forall (q0 : positive) (c0 : comparison), compare_cont c0 p q0 = switch_Eq c0 (compare_cont Eq p q0)
q:positive
c:comparison

switch_Eq Lt (switch_Eq Eq (compare_cont Eq p q)) = switch_Eq c (switch_Eq Lt (switch_Eq Eq (compare_cont Eq p q)))
now destruct (compare_cont Eq p q). Qed.
From this general result, we now describe particular cases of compare_cont p q c = c' :
p, q:positive
c:comparison

compare_cont c p q = Eq -> c = Eq
p, q:positive
c:comparison

compare_cont c p q = Eq -> c = Eq
p, q:positive
c:comparison

switch_Eq c (p ?= q) = Eq -> c = Eq
now destruct (p ?= q). Qed.
p, q:positive

compare_cont Lt p q = Gt <-> p > q
p, q:positive

compare_cont Lt p q = Gt <-> p > q
p, q:positive

switch_Eq Lt (p ?= q) = Gt <-> p > q
p, q:positive

switch_Eq Lt (p ?= q) = Gt <-> (p ?= q) = Gt
destruct (p ?= q); now split. Qed.
p, q:positive

compare_cont Lt p q = Lt <-> p <= q
p, q:positive

compare_cont Lt p q = Lt <-> p <= q
p, q:positive

switch_Eq Lt (p ?= q) = Lt <-> p <= q
p, q:positive

switch_Eq Lt (p ?= q) = Lt <-> (p ?= q) <> Gt
destruct (p ?= q); easy'. Qed.
p, q:positive

compare_cont Gt p q = Lt <-> p < q
p, q:positive

compare_cont Gt p q = Lt <-> p < q
p, q:positive

switch_Eq Gt (p ?= q) = Lt <-> p < q
p, q:positive

switch_Eq Gt (p ?= q) = Lt <-> (p ?= q) = Lt
destruct (p ?= q); now split. Qed.
p, q:positive

compare_cont Gt p q = Gt <-> p >= q
p, q:positive

compare_cont Gt p q = Gt <-> p >= q
p, q:positive

switch_Eq Gt (p ?= q) = Gt <-> p >= q
p, q:positive

switch_Eq Gt (p ?= q) = Gt <-> (p ?= q) <> Lt
destruct (p ?= q); easy'. Qed.
p, q:positive

compare_cont Lt p q <> Lt <-> p > q
p, q:positive

compare_cont Lt p q <> Lt <-> p > q
p, q:positive

~ p <= q <-> p > q
p, q:positive

~ compare_cont Eq p q <> Gt <-> compare_cont Eq p q = Gt
now destruct compare_cont; split; try apply comparison_eq_stable. Qed.
p, q:positive

compare_cont Lt p q <> Gt <-> p <= q
p, q:positive

compare_cont Lt p q <> Gt <-> p <= q
apply not_iff_compat, compare_cont_Lt_Gt. Qed.
p, q:positive

compare_cont Gt p q <> Lt <-> p >= q
p, q:positive

compare_cont Gt p q <> Lt <-> p >= q
apply not_iff_compat, compare_cont_Gt_Lt. Qed.
p, q:positive

compare_cont Gt p q <> Gt <-> p < q
p, q:positive

compare_cont Gt p q <> Gt <-> p < q
p, q:positive

~ p >= q <-> p < q
p, q:positive

~ compare_cont Eq p q <> Lt <-> compare_cont Eq p q = Lt
now destruct compare_cont; split; try apply comparison_eq_stable. Qed.
We can express recursive equations for compare
p, q:positive

(p~0 ?= q~0) = (p ?= q)
p, q:positive

(p~0 ?= q~0) = (p ?= q)
reflexivity. Qed.
p, q:positive

(p~1 ?= q~1) = (p ?= q)
p, q:positive

(p~1 ?= q~1) = (p ?= q)
reflexivity. Qed.
p, q:positive

(p~1 ?= q~0) = switch_Eq Gt (p ?= q)
p, q:positive

(p~1 ?= q~0) = switch_Eq Gt (p ?= q)
exact (compare_cont_spec p q Gt). Qed.
p, q:positive

(p~0 ?= q~1) = switch_Eq Lt (p ?= q)
p, q:positive

(p~0 ?= q~1) = switch_Eq Lt (p ?= q)
exact (compare_cont_spec p q Lt). Qed. 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.
Relation between compare and sub_mask
Definition mask2cmp (p:mask) : comparison :=
 match p with
  | IsNul => Eq
  | IsPos _ => Gt
  | IsNeg => Lt
 end.

p, q:positive

(p ?= q) = mask2cmp (sub_mask p q)
p, q:positive

(p ?= q) = mask2cmp (sub_mask p q)
p:positive

forall q : positive, (p ?= q) = mask2cmp (sub_mask p q)
induction p as [p IHp| p IHp| ]; intros [q|q| ]; simpl; trivial; specialize (IHp q); rewrite ?sub_mask_carry_spec; destruct (sub_mask p q) as [|r|]; simpl in *; try clear r; try destruct r; simpl; trivial; simpl_compare; now rewrite IHp. Qed.
Alternative characterisation of strict order in term of addition
p, q:positive

p < q <-> (exists r : positive, p + r = q)
p, q:positive

p < q <-> (exists r : positive, p + r = q)
p, q:positive

(p ?= q) = Lt <-> (exists r : positive, p + r = q)
p, q:positive

mask2cmp (sub_mask p q) = Lt <-> sub_mask p q = IsNeg
destruct sub_mask; now split. Qed.
p, q:positive

p > q <-> (exists r : positive, q + r = p)
p, q:positive

p > q <-> (exists r : positive, q + r = p)
p, q:positive

(p ?= q) = Gt <-> (exists r : positive, q + r = p)
p, q:positive

mask2cmp (sub_mask p q) = Gt <-> (exists r : positive, q + r = p)
p, q:positive

mask2cmp (sub_mask p q) = Gt -> exists r : positive, q + r = p
p, q:positive
(exists r : positive, q + r = p) -> mask2cmp (sub_mask p q) = Gt
p, q, r:positive
Hr:sub_mask p q = IsPos r

exists r0 : positive, q + r0 = p
p, q:positive
(exists r : positive, q + r = p) -> mask2cmp (sub_mask p q) = Gt
p, q, r:positive
Hr:sub_mask p q = IsPos r

q + r = p
p, q:positive
(exists r : positive, q + r = p) -> mask2cmp (sub_mask p q) = Gt
p, q:positive

(exists r : positive, q + r = p) -> mask2cmp (sub_mask p q) = Gt
p, q, r:positive
Hr:q + r = p

mask2cmp (sub_mask p q) = Gt
p, q, r:positive
Hr:sub_mask p q = IsPos r

mask2cmp (sub_mask p q) = Gt
now rewrite Hr. Qed.
Basic facts about compare_cont
p:positive
c:comparison

compare_cont c p p = c
p:positive
c:comparison

compare_cont c p p = c
now induction p. Qed.
p, q:positive
c:comparison

CompOpp (compare_cont c p q) = compare_cont (CompOpp c) q p
p, q:positive
c:comparison

CompOpp (compare_cont c p q) = compare_cont (CompOpp c) q p
p:positive

forall (q : positive) (c : comparison), CompOpp (compare_cont c p q) = compare_cont (CompOpp c) q p
induction p as [p IHp|p IHp| ]; intros [q|q| ] c; simpl; trivial; apply IHp. Qed.
Basic facts about compare
p, q:positive

(p ?= q) = Eq <-> p = q
p, q:positive

(p ?= q) = Eq <-> p = q
p, q:positive

mask2cmp (sub_mask p q) = Eq <-> sub_mask p q = IsNul
destruct sub_mask; now split. Qed.
p, q:positive

(q ?= p) = CompOpp (p ?= q)
p, q:positive

(q ?= p) = CompOpp (p ?= q)
p, q:positive

compare_cont Eq q p = CompOpp (compare_cont Eq p q)
now rewrite compare_cont_antisym. Qed.
p, q:positive

(p ?= q) = Lt <-> p < q
p, q:positive

(p ?= q) = Lt <-> p < q
reflexivity. Qed.
p, q:positive

(p ?= q) <> Gt <-> p <= q
p, q:positive

(p ?= q) <> Gt <-> p <= q
reflexivity. Qed.
More properties about compare and boolean comparisons, including compare_spec and lt_irrefl and lt_eq_cases.
Include BoolOrderFacts.

Definition le_lteq := lt_eq_cases.

Facts about gt and ge

The predicates lt and le are now favored in the statements of theorems, the use of gt and ge is hence not recommended. We provide here the bare minimal results to related them with lt and le.
p, q:positive

p > q <-> q < p
p, q:positive

p > q <-> q < p
p, q:positive

(p ?= q) = Gt <-> (q ?= p) = Lt
now rewrite compare_antisym, CompOpp_iff. Qed.
p, q:positive

p > q -> q < p
p, q:positive

p > q -> q < p
apply gt_lt_iff. Qed.
p, q:positive

p < q -> q > p
p, q:positive

p < q -> q > p
apply gt_lt_iff. Qed.
p, q:positive

p >= q <-> q <= p
p, q:positive

p >= q <-> q <= p
p, q:positive

(p ?= q) <> Lt <-> (q ?= p) <> Gt
now rewrite compare_antisym, CompOpp_iff. Qed.
p, q:positive

p >= q -> q <= p
p, q:positive

p >= q -> q <= p
apply ge_le_iff. Qed.
p, q:positive

p <= q -> q >= p
p, q:positive

p <= q -> q >= p
apply ge_le_iff. Qed.

Comparison and the successor

p, q:positive

switch_Eq Gt (p ?= succ q) = switch_Eq Lt (p ?= q)
p, q:positive

switch_Eq Gt (p ?= succ q) = switch_Eq Lt (p ?= q)
p:positive

forall q : positive, switch_Eq Gt (p ?= succ q) = switch_Eq Lt (p ?= q)
induction p as [p IH|p IH| ]; intros [q|q| ]; simpl; simpl_compare; rewrite ?IH; trivial; (now destruct compare) || (now destruct p). Qed.
p, q:positive

switch_Eq Lt (succ p ?= q) = switch_Eq Gt (p ?= q)
p, q:positive

switch_Eq Lt (succ p ?= q) = switch_Eq Gt (p ?= q)
p, q:positive

switch_Eq Lt (CompOpp (q ?= succ p)) = switch_Eq Gt (CompOpp (q ?= p))
p, q:positive

switch_Eq Gt (q ?= succ p) = switch_Eq Lt (q ?= p) -> switch_Eq Lt (CompOpp (q ?= succ p)) = switch_Eq Gt (CompOpp (q ?= p))
now do 2 destruct compare. Qed.
p, q:positive

p < succ q <-> p <= q
p, q:positive

p < succ q <-> p <= q
p, q:positive

(p ?= succ q) = Lt <-> (p ?= q) <> Gt
p, q:positive

switch_Eq Gt (p ?= succ q) = switch_Eq Lt (p ?= q) -> (p ?= succ q) = Lt <-> (p ?= q) <> Gt
do 2 destruct compare; try discriminate; now split. Qed.
p:positive

p < succ p
p:positive

p < succ p
p:positive

exists r : positive, p + r = succ p
p:positive

p + 1 = succ p
apply add_1_r. Qed.
p, q:positive

(succ p ?= succ q) = (p ?= q)
p, q:positive

(succ p ?= succ q) = (p ?= q)
p:positive

forall q : positive, (succ p ?= succ q) = (p ?= q)
induction p; destruct q; simpl; simpl_compare; trivial; apply compare_succ_l || apply compare_succ_r || (now destruct p) || (now destruct q). Qed.

1 is the least positive number

p:positive

1 <= p
p:positive

1 <= p
now destruct p. Qed.
p:positive

~ p < 1
p:positive

~ p < 1
now destruct p. Qed.
p:positive

1 < succ p
p:positive

1 < succ p
apply lt_succ_r, le_1_l. Qed.

Properties of the order

p, q:positive

p <= q <-> ~ q < p
p, q:positive

p <= q <-> ~ q < p
now rewrite <- ge_le_iff. Qed.
p, q:positive

p < q <-> ~ q <= p
p, q:positive

p < q <-> ~ q <= p
p, q:positive

p < q <-> ~ q <= p
p, q:positive

(p ?= q) = Lt <-> ~ (q ?= p) <> Gt
p, q:positive

CompOpp (q ?= p) = Lt <-> ~ (q ?= p) <> Gt
destruct compare; split; auto; easy'. Qed.
p, q:positive

p < q -> p <= q
p, q:positive

p < q -> p <= q
p, q:positive
H:p < q

p <= q
p, q:positive
H:p < q

p < q \/ p = q
now left. Qed.
n, m:positive

n < m -> n < succ m
n, m:positive

n < m -> n < succ m
n, m:positive
H:n < m

n < succ m
now apply lt_succ_r, lt_le_incl. Qed.
n, m:positive

n < m <-> succ n < succ m
n, m:positive

n < m <-> succ n < succ m
n, m:positive

(n ?= m) = Lt <-> (succ n ?= succ m) = Lt
now rewrite compare_succ_succ. Qed.
n, m:positive

n <= m <-> succ n <= succ m
n, m:positive

n <= m <-> succ n <= succ m
n, m:positive

(n ?= m) <> Gt <-> (succ n ?= succ m) <> Gt
now rewrite compare_succ_succ. Qed.
n, m, p:positive

n < m -> m < p -> n < p
n, m, p:positive

n < m -> m < p -> n < p
n, m, p:positive

(exists r : positive, n + r = m) -> (exists r : positive, m + r = p) -> exists r : positive, n + r = p
n, m, p, r:positive
Hr:n + r = m
s:positive
Hs:m + s = p

exists r0 : positive, n + r0 = p
n, m, p, r:positive
Hr:n + r = m
s:positive
Hs:m + s = p

n + (r + s) = p
now rewrite add_assoc, Hr, Hs. Qed.

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

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
A:positive -> Prop
n:positive
AB:A (succ n)
AS:forall m0 : positive, n < m0 -> A m0 -> A (succ m0)
m:positive

n < m -> A m
A:positive -> Prop
n:positive
AB:A (succ n)
AS:forall m : positive, n < m -> A m -> A (succ m)
H:n < 1

A 1
A:positive -> Prop
n:positive
AB:A (succ n)
AS:forall m0 : positive, n < m0 -> A m0 -> A (succ m0)
m:positive
IHm:n < m -> A m
H:n < succ m
A (succ m)
A:positive -> Prop
n:positive
AB:A (succ n)
AS:forall m0 : positive, n < m0 -> A m0 -> A (succ m0)
m:positive
IHm:n < m -> A m
H:n < succ m

A (succ m)
A:positive -> Prop
n:positive
AB:A (succ n)
AS:forall m0 : positive, n < m0 -> A m0 -> A (succ m0)
m:positive
IHm:n < m -> A m
H:n < m \/ n = m

A (succ m)
destruct H as [H|H]; subst; auto. Qed.

StrictOrder lt

StrictOrder lt

Irreflexive lt

Transitive lt

Transitive lt
exact lt_trans. Qed.

Proper (Logic.eq ==> Logic.eq ==> iff) lt

Proper (Logic.eq ==> Logic.eq ==> iff) lt

forall x y : positive, x = y -> forall x0 y0 : positive, x0 = y0 -> (x < x0 -> y < y0) /\ (y < y0 -> x < x0)
x, y:positive
H:x = y
x0, y0:positive
H0:x0 = y0

(x < x0 -> y < y0) /\ (y < y0 -> x < x0)
subst; auto. Qed.
p, q:positive

p < q \/ p = q \/ q < p
p, q:positive

p < q \/ p = q \/ q < p
case (compare_spec p q); intuition. Qed.
p:positive

p <= p
p:positive

p <= p
p:positive

p <= p
p:positive

(p ?= p) <> Gt
now rewrite compare_refl. Qed.
n, m, p:positive

n <= m -> m < p -> n < p
n, m, p:positive

n <= m -> m < p -> n < p
n, m, p:positive
H:n <= m
H':m < p

n < p
n, m, p:positive
H:n < m \/ n = m
H':m < p

n < p
n, m, p:positive
H:n < m
H':m < p

n < p
n, m, p:positive
H:n = m
H':m < p
n < p
n, m, p:positive
H:n = m
H':m < p

n < p
now subst. Qed.
n, m, p:positive

n < m -> m <= p -> n < p
n, m, p:positive

n < m -> m <= p -> n < p
n, m, p:positive
H:n < m
H':m <= p

n < p
n, m, p:positive
H:n < m
H':m < p \/ m = p

n < p
n, m, p:positive
H:n < m
H0:m < p

n < p
n, m, p:positive
H:n < m
H0:m = p
n < p
n, m, p:positive
H:n < m
H0:m = p

n < p
now subst. Qed.
n, m, p:positive

n <= m -> m <= p -> n <= p
n, m, p:positive

n <= m -> m <= p -> n <= p
n, m, p:positive
H:n <= m
H':m <= p

n <= p
n, m, p:positive
H:n < m \/ n = m
H':m <= p

n <= p
n, m, p:positive
H:n < m
H':m <= p

n <= p
n, m, p:positive
H:n = m
H':m <= p
n <= p
n, m, p:positive
H:n < m
H':m <= p

n < p
n, m, p:positive
H:n = m
H':m <= p
n <= p
n, m, p:positive
H:n = m
H':m <= p

n <= p
now subst. Qed.
n, m:positive

succ n <= m <-> n < m
n, m:positive

succ n <= m <-> n < m
n, m:positive

succ n < succ m <-> n < m
n, m:positive

n < m <-> succ n < succ m
apply succ_lt_mono. Qed.
p, q:positive

p <= q -> q <= p -> p = q
p, q:positive

p <= q -> q <= p -> p = q
p, q:positive
H:p < q

q <= p -> p = q
p, q:positive
H:p < q
H0:q < p

p = q
p, q:positive
H:p < q
H0:q < p

p < p
now transitivity q. Qed.

PreOrder le

PreOrder le

Reflexive le

Transitive le

Transitive le
exact le_trans. Qed.

PartialOrder Logic.eq le

PartialOrder Logic.eq le
x, y:positive

pointwise_lifting iff Tnil (x = y) (relation_conjunction le (Basics.flip le) x y)
x, y:positive

x = y <-> x <= y <= x
x, y:positive

x = y -> x <= y <= x
x, y:positive
x <= y <= x -> x = y
x, y:positive

x <= y <= x -> x = y
destruct 1; now apply le_antisym. Qed.

Comparison and addition

p, q, r:positive

(p + q ?= p + r) = (q ?= r)
p, q, r:positive

(p + q ?= p + r) = (q ?= r)

forall p q r : positive, (p + q ?= p + r) = (q ?= r)
q, r:positive

(1 + q ?= 1 + r) = (q ?= r)
p:positive
IHp:forall q0 r0 : positive, (p + q0 ?= p + r0) = (q0 ?= r0)
q, r:positive
(succ p + q ?= succ p + r) = (q ?= r)
q, r:positive

(succ q ?= succ r) = (q ?= r)
p:positive
IHp:forall q0 r0 : positive, (p + q0 ?= p + r0) = (q0 ?= r0)
q, r:positive
(succ p + q ?= succ p + r) = (q ?= r)
p:positive
IHp:forall q0 r0 : positive, (p + q0 ?= p + r0) = (q0 ?= r0)
q, r:positive

(succ p + q ?= succ p + r) = (q ?= r)
now rewrite 2 add_succ_l, compare_succ_succ. Qed.
p, q, r:positive

(q + p ?= r + p) = (q ?= r)
p, q, r:positive

(q + p ?= r + p) = (q ?= r)
p, q, r:positive

(p + q ?= p + r) = (q ?= r)
apply add_compare_mono_l. Qed.

Order and addition

p, q:positive

p < p + q
p, q:positive

p < p + q
p, q:positive

exists r : positive, p + r = p + q
now exists q. Qed.
p, q, r:positive

q < r <-> p + q < p + r
p, q, r:positive

q < r <-> p + q < p + r
p, q, r:positive

(q ?= r) = Lt <-> (p + q ?= p + r) = Lt
p, q, r:positive

(q ?= r) = Lt <-> (q ?= r) = Lt
apply iff_refl. Qed.
p, q, r:positive

q < r <-> q + p < r + p
p, q, r:positive

q < r <-> q + p < r + p
p, q, r:positive

(q ?= r) = Lt <-> (q + p ?= r + p) = Lt
p, q, r:positive

(q ?= r) = Lt <-> (q ?= r) = Lt
apply iff_refl. Qed.
p, q, r, s:positive

p < q -> r < s -> p + r < q + s
p, q, r, s:positive

p < q -> r < s -> p + r < q + s
p, q, r, s:positive
H:p < q
H0:r < s

p + r < q + s
p, q, r, s:positive
H:p < q
H0:r < s

p + r < p + s
p, q, r, s:positive
H:p < q
H0:r < s
p + s < q + s
p, q, r, s:positive
H:p < q
H0:r < s

p + s < q + s
now apply add_lt_mono_r. Qed.
p, q, r:positive

q <= r <-> p + q <= p + r
p, q, r:positive

q <= r <-> p + q <= p + r
p, q, r:positive

(q ?= r) <> Gt <-> (p + q ?= p + r) <> Gt
p, q, r:positive

(q ?= r) <> Gt <-> (q ?= r) <> Gt
apply iff_refl. Qed.
p, q, r:positive

q <= r <-> q + p <= r + p
p, q, r:positive

q <= r <-> q + p <= r + p
p, q, r:positive

(q ?= r) <> Gt <-> (q + p ?= r + p) <> Gt
p, q, r:positive

(q ?= r) <> Gt <-> (q ?= r) <> Gt
apply iff_refl. Qed.
p, q, r, s:positive

p <= q -> r <= s -> p + r <= q + s
p, q, r, s:positive

p <= q -> r <= s -> p + r <= q + s
p, q, r, s:positive
H:p <= q
H0:r <= s

p + r <= q + s
p, q, r, s:positive
H:p <= q
H0:r <= s

p + r <= p + s
p, q, r, s:positive
H:p <= q
H0:r <= s
p + s <= q + s
p, q, r, s:positive
H:p <= q
H0:r <= s

p + s <= q + s
now apply add_le_mono_r. Qed.

Comparison and multiplication

p, q, r:positive

(p * q ?= p * r) = (q ?= r)
p, q, r:positive

(p * q ?= p * r) = (q ?= r)
p:positive

forall q r : positive, (p * q ?= p * r) = (q ?= r)
p:positive
IHp:forall q r : positive, (p * q ?= p * r) = (q ?= r)

forall q r : positive, (q + (p * q)~0 ?= r + (p * r)~0) = (q ?= r)
p:positive
IHp:forall q0 r0 : positive, (p * q0 ?= p * r0) = (q0 ?= r0)
q, r:positive

(q + (p * q)~0 ?= r + (p * r)~0) = (q ?= r)
p, q, r:positive
IHp:(p * q ?= p * r) = (q ?= r)

(q + (p * q)~0 ?= r + (p * r)~0) = (q ?= r)
p, q, r:positive
IHp:(p * q ?= p * r) = Eq
H:q = r

(q + (p * q)~0 ?= r + (p * r)~0) = Eq
p, q, r:positive
IHp:(p * q ?= p * r) = Lt
H:q < r
(q + (p * q)~0 ?= r + (p * r)~0) = Lt
p, q, r:positive
IHp:(p * q ?= p * r) = Gt
H:r < q
(q + (p * q)~0 ?= r + (p * r)~0) = Gt
p, r:positive
IHp:(p * r ?= p * r) = Eq

(r + (p * r)~0 ?= r + (p * r)~0) = Eq
p, q, r:positive
IHp:(p * q ?= p * r) = Lt
H:q < r
(q + (p * q)~0 ?= r + (p * r)~0) = Lt
p, q, r:positive
IHp:(p * q ?= p * r) = Gt
H:r < q
(q + (p * q)~0 ?= r + (p * r)~0) = Gt
p, q, r:positive
IHp:(p * q ?= p * r) = Lt
H:q < r

(q + (p * q)~0 ?= r + (p * r)~0) = Lt
p, q, r:positive
IHp:(p * q ?= p * r) = Gt
H:r < q
(q + (p * q)~0 ?= r + (p * r)~0) = Gt
p, q, r:positive
IHp:(p * q ?= p * r) = Gt
H:r < q

(q + (p * q)~0 ?= r + (p * r)~0) = Gt
now apply lt_gt, add_lt_mono, gt_lt. Qed.
p, q, r:positive

(q * p ?= r * p) = (q ?= r)
p, q, r:positive

(q * p ?= r * p) = (q ?= r)
p, q, r:positive

(p * q ?= p * r) = (q ?= r)
apply mul_compare_mono_l. Qed.

Order and multiplication

p, q, r:positive

q < r <-> p * q < p * r
p, q, r:positive

q < r <-> p * q < p * r
p, q, r:positive

(q ?= r) = Lt <-> (p * q ?= p * r) = Lt
p, q, r:positive

(q ?= r) = Lt <-> (q ?= r) = Lt
apply iff_refl. Qed.
p, q, r:positive

q < r <-> q * p < r * p
p, q, r:positive

q < r <-> q * p < r * p
p, q, r:positive

(q ?= r) = Lt <-> (q * p ?= r * p) = Lt
p, q, r:positive

(q ?= r) = Lt <-> (q ?= r) = Lt
apply iff_refl. Qed.
p, q, r, s:positive

p < q -> r < s -> p * r < q * s
p, q, r, s:positive

p < q -> r < s -> p * r < q * s
p, q, r, s:positive
H:p < q
H0:r < s

p * r < q * s
p, q, r, s:positive
H:p < q
H0:r < s

p * r < p * s
p, q, r, s:positive
H:p < q
H0:r < s
p * s < q * s
p, q, r, s:positive
H:p < q
H0:r < s

p * s < q * s
now apply mul_lt_mono_r. Qed.
p, q, r:positive

q <= r <-> p * q <= p * r
p, q, r:positive

q <= r <-> p * q <= p * r
p, q, r:positive

(q ?= r) <> Gt <-> (p * q ?= p * r) <> Gt
p, q, r:positive

(q ?= r) <> Gt <-> (q ?= r) <> Gt
apply iff_refl. Qed.
p, q, r:positive

q <= r <-> q * p <= r * p
p, q, r:positive

q <= r <-> q * p <= r * p
p, q, r:positive

(q ?= r) <> Gt <-> (q * p ?= r * p) <> Gt
p, q, r:positive

(q ?= r) <> Gt <-> (q ?= r) <> Gt
apply iff_refl. Qed.
p, q, r, s:positive

p <= q -> r <= s -> p * r <= q * s
p, q, r, s:positive

p <= q -> r <= s -> p * r <= q * s
p, q, r, s:positive
H:p <= q
H0:r <= s

p * r <= q * s
p, q, r, s:positive
H:p <= q
H0:r <= s

p * r <= p * s
p, q, r, s:positive
H:p <= q
H0:r <= s
p * s <= q * s
p, q, r, s:positive
H:p <= q
H0:r <= s

p * s <= q * s
now apply mul_le_mono_r. Qed.
p, q:positive

p < p + q
p, q:positive

p < p + q
p:positive

p < p + 1
p, q:positive
IHq:p < p + q
p < p + succ q
p:positive

p < succ p
p, q:positive
IHq:p < p + q
p < p + succ q
p, q:positive
IHq:p < p + q

p < p + succ q
p, q:positive
IHq:p < p + q

p + q < p + succ q
apply add_lt_mono_l, lt_succ_diag_r. Qed.
p, q:positive

~ p + q < p
p, q:positive

~ p + q < p
p, q:positive
H:p + q < p

False
p, q:positive
H:p + q < p

p < p
apply lt_trans with (p+q); auto using lt_add_r. Qed.
n, p:positive

1 < n -> 1 < n ^ p
n, p:positive

1 < n -> 1 < n ^ p
n, p:positive
H:1 < n

1 < n ^ p
n:positive
H:1 < n

1 < n ^ 1
n, p:positive
H:1 < n
IHp:1 < n ^ p
1 < n ^ succ p
n, p:positive
H:1 < n
IHp:1 < n ^ p

1 < n ^ succ p
n, p:positive
H:1 < n
IHp:1 < n ^ p

1 < n * n ^ p
n, p:positive
H:1 < n
IHp:1 < n ^ p

1 < n * 1
n, p:positive
H:1 < n
IHp:1 < n ^ p
n * 1 < n * n ^ p
n, p:positive
H:1 < n
IHp:1 < n ^ p

n * 1 < n * n ^ p
now apply mul_lt_mono_l. Qed. (**********************************************************************)

Properties of subtraction on binary positive numbers

p:positive

p - 1 = pred p
p:positive

p - 1 = pred p
now destruct p. Qed.
p:positive

pred p = p - 1
p:positive

pred p = p - 1
p:positive

p - 1 = pred p
apply sub_1_r. Qed.
p, q:positive

p - succ q = pred (p - q)
p, q:positive

p - succ q = pred (p - q)
p, q:positive

match pred_mask (sub_mask p q) with | IsPos z => z | _ => 1 end = pred match sub_mask p q with | IsPos z => z | _ => 1 end
destruct (sub_mask p q) as [|[r|r| ]|]; auto. Qed.

Properties of subtraction without underflow

p, q:positive

q < p -> exists r : positive, sub_mask p q = IsPos r /\ q + r = p
p, q:positive

q < p -> exists r : positive, sub_mask p q = IsPos r /\ q + r = p
p, q:positive

(exists r : positive, q + r = p) -> exists r : positive, sub_mask p q = IsPos r /\ q + r = p
p, q, r:positive
Hr:q + r = p

exists r0 : positive, sub_mask p q = IsPos r0 /\ q + r0 = p
p, q, r:positive
Hr:q + r = p

sub_mask p q = IsPos r /\ q + r = p
p, q, r:positive
Hr:q + r = p

sub_mask p q = IsPos r
now apply sub_mask_pos_iff. Qed.
p, q:positive

q < p -> exists r : positive, sub_mask p q = IsPos r
p, q:positive

q < p -> exists r : positive, sub_mask p q = IsPos r
p, q:positive
H:q < p

exists r : positive, sub_mask p q = IsPos r
p, q:positive
H:q < p
r:positive
Hr:sub_mask p q = IsPos r

exists r0 : positive, sub_mask p q = IsPos r0
now exists r. Qed.
p, q:positive

q < p -> p - q + q = p
p, q:positive

q < p -> p - q + q = p
p, q:positive
H:q < p

p - q + q = p
p, q:positive
H:q < p
r:positive
U:sub_mask p q = IsPos r

p - q + q = p
p, q:positive
H:q < p
r:positive
U:sub_mask p q = IsPos r

match sub_mask p q with | IsPos z => z | _ => 1 end + q = p
p, q:positive
H:q < p
r:positive
U:sub_mask p q = IsPos r

r + q = p
p, q:positive
H:q < p
r:positive
U:sub_mask p q = IsPos r

q + r = p
now apply sub_mask_add. Qed.
p, q:positive

p + q - q = p
p, q:positive

p + q - q = p
p, q:positive

p + q - q = p
p, q:positive

p + q - q + q = p + q
p, q:positive

q < p + q
p, q:positive

q < q + p
apply lt_add_r. Qed.
p, q, r:positive

r < q -> p * (q - r) = p * q - p * r
p, q, r:positive

r < q -> p * (q - r) = p * q - p * r
p, q, r:positive
H:r < q

p * (q - r) = p * q - p * r
p, q, r:positive
H:r < q

p * (q - r) + p * r = p * q - p * r + p * r
p, q, r:positive
H:r < q

p * (q - r + r) = p * q - p * r + p * r
p, q, r:positive
H:r < q

p * q = p * q - p * r + p * r
p, q, r:positive
H:r < q

p * q - p * r + p * r = p * q
p, q, r:positive
H:r < q

p * r < p * q
now apply mul_lt_mono_l. Qed.
p, q, r:positive

q < p -> (p - q) * r = p * r - q * r
p, q, r:positive

q < p -> (p - q) * r = p * r - q * r
p, q, r:positive
H:q < p

(p - q) * r = p * r - q * r
p, q, r:positive
H:q < p

r * (p - q) = r * p - r * q
now apply mul_sub_distr_l. Qed.
p, q, r:positive

q < p -> p < r -> r - p < r - q
p, q, r:positive

q < p -> p < r -> r - p < r - q
p, q, r:positive
Hqp:q < p
Hpr:p < r

r - p < r - q
p, q, r:positive
Hqp:q < p
Hpr:p < r

r - p + p < r - q + p
p, q, r:positive
Hqp:q < p
Hpr:p < r

r < r - q + p
p, q, r:positive
Hqp:q < p
Hpr:p < r

r <= r - q + q
p, q, r:positive
Hqp:q < p
Hpr:p < r
r - q + q < r - q + p
p, q, r:positive
Hqp:q < p
Hpr:p < r

r <= r
p, q, r:positive
Hqp:q < p
Hpr:p < r
r - q + q < r - q + p
p, q, r:positive
Hqp:q < p
Hpr:p < r

r - q + q < r - q + p
now apply add_lt_mono_l. Qed.
p, q, r:positive

q < p -> r < p -> (p - q ?= p - r) = (r ?= q)
p, q, r:positive

q < p -> r < p -> (p - q ?= p - r) = (r ?= q)
p, q, r:positive
Hqp:q < p
Hrp:r < p

(p - q ?= p - r) = (r ?= q)
p, q, r:positive
Hqp:q < p
Hrp:r < p
H:r = q

(p - q ?= p - r) = Eq
p, q, r:positive
Hqp:q < p
Hrp:r < p
H:r < q
(p - q ?= p - r) = Lt
p, q, r:positive
Hqp:q < p
Hrp:r < p
H:q < r
(p - q ?= p - r) = Gt
p, q:positive
Hqp, Hrp:q < p

(p - q ?= p - q) = Eq
p, q, r:positive
Hqp:q < p
Hrp:r < p
H:r < q
(p - q ?= p - r) = Lt
p, q, r:positive
Hqp:q < p
Hrp:r < p
H:q < r
(p - q ?= p - r) = Gt
p, q, r:positive
Hqp:q < p
Hrp:r < p
H:r < q

(p - q ?= p - r) = Lt
p, q, r:positive
Hqp:q < p
Hrp:r < p
H:q < r
(p - q ?= p - r) = Gt
p, q, r:positive
Hqp:q < p
Hrp:r < p
H:q < r

(p - q ?= p - r) = Gt
apply lt_gt, sub_lt_mono_l; trivial. Qed.
p, q, r:positive

p < q -> p < r -> (q - p ?= r - p) = (q ?= r)
p, q, r:positive

p < q -> p < r -> (q - p ?= r - p) = (q ?= r)
p, q, r:positive
H:p < q
H0:p < r

(q - p ?= r - p) = (q ?= r)
rewrite <- (add_compare_mono_r p), 2 sub_add; trivial. Qed.
p, q, r:positive

q < p -> r < q -> q - r < p - r
p, q, r:positive

q < p -> r < q -> q - r < p - r
p, q, r:positive
H:q < p
H0:r < q

q - r < p - r
p, q, r:positive
H:q < p
H0:r < q

(q - r ?= p - r) = Lt
p, q, r:positive
H:q < p
H0:r < q

r < p
now apply lt_trans with q. Qed.
n, m:positive

m < n -> n - m < n
n, m:positive

m < n -> n - m < n
n, m:positive
H:m < n

n - m < n
n, m:positive
H:m < n

n - m + m < n + m
n, m:positive
H:m < n

n < n + m
apply lt_add_r. Qed.
p, q, r:positive

r < q -> p + (q - r) = p + q - r
p, q, r:positive

r < q -> p + (q - r) = p + q - r
p, q, r:positive
H:r < q

p + (q - r) = p + q - r
p, q, r:positive
H:r < q

p + (q - r) + r = p + q - r + r
p, q, r:positive
H:r < q

r < p + q
p, q, r:positive
H:r < q

r < q + p
apply lt_trans with q; trivial using lt_add_r. Qed.
p, q, r:positive

q + r < p -> p - (q + r) = p - q - r
p, q, r:positive

q + r < p -> p - (q + r) = p - q - r
p, q, r:positive
H:q + r < p

p - (q + r) = p - q - r
p, q, r:positive
H:q + r < p
H0:q < p

p - (q + r) = p - q - r
p, q, r:positive
H:r + q < p
H0:q < p

p - (r + q) = p - q - r
p, q, r:positive
H:r + q < p
H0:q < p

p - (r + q) + (r + q) = p - q - r + (r + q)
p, q, r:positive
H:r + q < p
H0:q < p

p = p - q - r + (r + q)
p, q, r:positive
H:r + q < p
H0:q < p

r < p - q
p, q, r:positive
H:r + q < p
H0:q < p

r + q < p - q + q
rewrite sub_add; trivial. Qed.
p, q, r:positive

r < q -> q - r < p -> p - (q - r) = p + r - q
p, q, r:positive

r < q -> q - r < p -> p - (q - r) = p + r - q
p, q, r:positive
H:r < q
H0:q - r < p

p - (q - r) = p + r - q
p, q, r:positive
H:r < q
H0:q - r < p

p - (q - r) + (q - r + r) = p + r - q + (q - r + r)
p, q, r:positive
H:r < q
H0:q - r < p

q < p + r
p, q, r:positive
H:r < q
H0:q - r < p

q - r + r < p + r
now apply add_lt_mono_r. Qed.
Recursive equations for sub
n, m:positive

m < n -> n~0 - m~0 = (n - m)~0
n, m:positive

m < n -> n~0 - m~0 = (n - m)~0
n, m:positive
H:m < n

n~0 - m~0 = (n - m)~0
n, m:positive
H:m < n

match sub_mask n~0 m~0 with | IsPos z => z | _ => 1 end = match sub_mask n m with | IsPos z => z | _ => 1 end~0
n, m:positive
H:m < n

match double_mask (sub_mask n m) with | IsPos z => z | _ => 1 end = match sub_mask n m with | IsPos z => z | _ => 1 end~0
now destruct (sub_mask_pos n m H) as (p, ->). Qed.
n, m:positive

m < n -> n~1 - m~1 = (n - m)~0
n, m:positive

m < n -> n~1 - m~1 = (n - m)~0
n, m:positive
H:m < n

n~1 - m~1 = (n - m)~0
n, m:positive
H:m < n

match sub_mask n~1 m~1 with | IsPos z => z | _ => 1 end = match sub_mask n m with | IsPos z => z | _ => 1 end~0
n, m:positive
H:m < n

match double_mask (sub_mask n m) with | IsPos z => z | _ => 1 end = match sub_mask n m with | IsPos z => z | _ => 1 end~0
now destruct (sub_mask_pos n m H) as (p, ->). Qed.
n, m:positive

m < n -> n~1 - m~0 = (n - m)~1
n, m:positive

m < n -> n~1 - m~0 = (n - m)~1
n, m:positive
H:m < n

n~1 - m~0 = (n - m)~1
n, m:positive
H:m < n

match sub_mask n~1 m~0 with | IsPos z => z | _ => 1 end = match sub_mask n m with | IsPos z => z | _ => 1 end~1
n, m:positive
H:m < n

match succ_double_mask (sub_mask n m) with | IsPos z => z | _ => 1 end = match sub_mask n m with | IsPos z => z | _ => 1 end~1
now destruct (sub_mask_pos n m) as (p, ->). Qed.
n, m:positive

n~0 - m~1 = pred_double (n - m)
n, m:positive

n~0 - m~1 = pred_double (n - m)
n, m:positive

match sub_mask n~0 m~1 with | IsPos z => z | _ => 1 end = pred_double match sub_mask n m with | IsPos z => z | _ => 1 end
n, m:positive

match succ_double_mask (sub_mask_carry n m) with | IsPos z => z | _ => 1 end = pred_double match sub_mask n m with | IsPos z => z | _ => 1 end
n, m:positive

match succ_double_mask (pred_mask (sub_mask n m)) with | IsPos z => z | _ => 1 end = pred_double match sub_mask n m with | IsPos z => z | _ => 1 end
now destruct (sub_mask n m) as [|[r|r|]|]. Qed.
Properties of subtraction with underflow
p, q:positive

sub_mask p q = IsNeg <-> p < q
p, q:positive

sub_mask p q = IsNeg <-> p < q
p, q:positive

sub_mask p q = IsNeg <-> (exists r : positive, p + r = q)
apply sub_mask_neg_iff. Qed.
p, q:positive

p < q -> sub_mask p q = IsNeg
p, q:positive

p < q -> sub_mask p q = IsNeg
apply sub_mask_neg_iff'. Qed.
p, q:positive

p <= q -> p - q = 1
p, q:positive

p <= q -> p - q = 1
p, q:positive

(p ?= q) <> Gt -> match sub_mask p q with | IsPos z => z | _ => 1 end = 1
p, q:positive

mask2cmp (sub_mask p q) <> Gt -> match sub_mask p q with | IsPos z => z | _ => 1 end = 1
destruct sub_mask; easy'. Qed.
p, q:positive

p < q -> p - q = 1
p, q:positive

p < q -> p - q = 1
p, q:positive
H:p < q

p - q = 1
now apply sub_le, lt_le_incl. Qed.
p:positive

p - p = 1
p:positive

p - p = 1
p:positive

match sub_mask p p with | IsPos z => z | _ => 1 end = 1
now rewrite sub_mask_diag. Qed.

Results concerning size and size_nat

p, q:positive

p < q -> (size_nat p <= size_nat q)%nat
p, q:positive

p < q -> (size_nat p <= size_nat q)%nat
p, q:positive
le0:forall n : nat, (0 <= n)%nat

p < q -> (size_nat p <= size_nat q)%nat
p, q:positive
le0:forall n : nat, (0 <= n)%nat
leS:forall n m : nat, (n <= m)%nat -> (S n <= S m)%nat

p < q -> (size_nat p <= size_nat q)%nat
p:positive
le0:forall n : nat, (0 <= n)%nat
leS:forall n m : nat, (n <= m)%nat -> (S n <= S m)%nat

forall q : positive, p < q -> (size_nat p <= size_nat q)%nat
p:positive
le0:forall n : nat, (0 <= n)%nat
leS:forall n m : nat, (n <= m)%nat -> (S n <= S m)%nat
IHp:forall q0 : positive, p < q0 -> (size_nat p <= size_nat q0)%nat
q:positive
H:switch_Eq Gt (p ?= q) = Lt

(size_nat p <= size_nat q)%nat
p:positive
le0:forall n : nat, (0 <= n)%nat
leS:forall n m : nat, (n <= m)%nat -> (S n <= S m)%nat
IHp:forall q0 : positive, p < q0 -> (size_nat p <= size_nat q0)%nat
q:positive
H:switch_Eq Lt (p ?= q) = Lt
(size_nat p <= size_nat q)%nat
p:positive
le0:forall n : nat, (0 <= n)%nat
leS:forall n m : nat, (n <= m)%nat -> (S n <= S m)%nat
IHp:forall q0 : positive, p < q0 -> (size_nat p <= size_nat q0)%nat
q:positive
H:switch_Eq Gt (p ?= q) = Lt

p < q
p:positive
le0:forall n : nat, (0 <= n)%nat
leS:forall n m : nat, (n <= m)%nat -> (S n <= S m)%nat
IHp:forall q0 : positive, p < q0 -> (size_nat p <= size_nat q0)%nat
q:positive
H:switch_Eq Lt (p ?= q) = Lt
(size_nat p <= size_nat q)%nat
p:positive
le0:forall n : nat, (0 <= n)%nat
leS:forall n m : nat, (n <= m)%nat -> (S n <= S m)%nat
IHp:forall q0 : positive, p < q0 -> (size_nat p <= size_nat q0)%nat
q:positive
H:switch_Eq Gt (p ?= q) = Lt

(p ?= q) = Lt
p:positive
le0:forall n : nat, (0 <= n)%nat
leS:forall n m : nat, (n <= m)%nat -> (S n <= S m)%nat
IHp:forall q0 : positive, p < q0 -> (size_nat p <= size_nat q0)%nat
q:positive
H:switch_Eq Lt (p ?= q) = Lt
(size_nat p <= size_nat q)%nat
p:positive
le0:forall n : nat, (0 <= n)%nat
leS:forall n m : nat, (n <= m)%nat -> (S n <= S m)%nat
IHp:forall q0 : positive, p < q0 -> (size_nat p <= size_nat q0)%nat
q:positive
H:switch_Eq Lt (p ?= q) = Lt

(size_nat p <= size_nat q)%nat
destruct (compare_spec p q); subst; now auto. Qed.
p:positive

p < 2 ^ size p
p:positive

p < 2 ^ size p
p:positive
IHp:p < 2 ^ size p

p~1 < 2 * 2 ^ size p
p:positive
IHp:succ p <= 2 ^ size p

p~1 < 2 * 2 ^ size p
now apply le_succ_l. Qed.
p:positive

2 ^ size p <= p~0
p:positive

2 ^ size p <= p~0
p:positive
IHp:2 ^ size p <= p~0

2 * 2 ^ size p <= p~1~0
p:positive
IHp:2 ^ size p <= p~0

2 ^ size p <= p~1
p:positive
IHp:2 ^ size p <= p~0

2 ^ size p < p~1
p:positive
IHp:2 ^ size p <= p~0

2 ^ size p < succ p~0
apply lt_succ_r, IHp. Qed.

Properties of min and max

First, the specification

forall x y : positive, y <= x -> max x y = x

forall x y : positive, y <= x -> max x y = x
x, y:positive
H:y <= x

max x y = x
x, y:positive
H:y <= x

match x ?= y with | Gt => x | _ => y end = x
x, y:positive
H:y <= x

x < y -> y = x
x, y:positive
H:y <= x
H':x < y

y = x
x, y:positive
H:~ x < y
H':x < y

y = x
now elim H. Qed.

forall x y : positive, x <= y -> max x y = y

forall x y : positive, x <= y -> max x y = y

forall x y : positive, (x ?= y) <> Gt -> match x ?= y with | Gt => x | _ => y end = y
x, y:positive

(x ?= y) <> Gt -> match x ?= y with | Gt => x | _ => y end = y
destruct compare; easy'. Qed.

forall x y : positive, x <= y -> min x y = x

forall x y : positive, x <= y -> min x y = x

forall x y : positive, (x ?= y) <> Gt -> match x ?= y with | Gt => y | _ => x end = x
x, y:positive

(x ?= y) <> Gt -> match x ?= y with | Gt => y | _ => x end = x
destruct compare; easy'. Qed.

forall x y : positive, y <= x -> min x y = y

forall x y : positive, y <= x -> min x y = y
x, y:positive
H:y <= x

min x y = y
x, y:positive
H:y <= x

match x ?= y with | Gt => y | _ => x end = y
x, y:positive
H:y <= x

x < y -> x = y
x, y:positive
H:y <= x
H':x < y

x = y
x, y:positive
H:~ x < y
H':x < y

x = y
now elim H'. Qed.
We hence obtain all the generic properties of min and max.
Include UsualMinMaxLogicalProperties <+ UsualMinMaxDecProperties.

Ltac order := Private_Tac.order.
Minimum, maximum and constant one
n:positive

max 1 n = n
n:positive

max 1 n = n
n:positive

match 1 ?= n with | Gt => 1 | _ => n end = n
n:positive

n < 1 -> 1 = n
n:positive
H:n < 1

1 = n
n:positive
H:~ 1 <= n

1 = n
n:positive
H:~ 1 <= n

1 <= n
apply le_1_l. Qed.
n:positive

max n 1 = n
n:positive

max n 1 = n
n:positive

max 1 n = n
apply max_1_l. Qed.
n:positive

min 1 n = 1
n:positive

min 1 n = 1
n:positive

match 1 ?= n with | Gt => n | _ => 1 end = 1
n:positive

n < 1 -> n = 1
n:positive
H:n < 1

n = 1
n:positive
H:~ 1 <= n

n = 1
n:positive
H:~ 1 <= n

1 <= n
apply le_1_l. Qed.
n:positive

min n 1 = 1
n:positive

min n 1 = 1
n:positive

min 1 n = 1
apply min_1_l. Qed.
Minimum, maximum and operations (consequences of monotonicity)
n, m:positive

succ (max n m) = max (succ n) (succ m)
n, m:positive

succ (max n m) = max (succ n) (succ m)
n, m:positive

max (succ n) (succ m) = succ (max n m)
n, m:positive

Proper (le ==> le) succ
n, m, x, x':positive

x <= x' -> succ x <= succ x'
apply succ_le_mono. Qed.
n, m:positive

succ (min n m) = min (succ n) (succ m)
n, m:positive

succ (min n m) = min (succ n) (succ m)
n, m:positive

min (succ n) (succ m) = succ (min n m)
n, m:positive

Proper (le ==> le) succ
n, m, x, x':positive

x <= x' -> succ x <= succ x'
apply succ_le_mono. Qed.
n, m, p:positive

max (p + n) (p + m) = p + max n m
n, m, p:positive

max (p + n) (p + m) = p + max n m
n, m, p:positive

Proper (le ==> le) (add p)
n, m, p, x, x':positive

x <= x' -> p + x <= p + x'
apply add_le_mono_l. Qed.
n, m, p:positive

max (n + p) (m + p) = max n m + p
n, m, p:positive

max (n + p) (m + p) = max n m + p
n, m, p:positive

max (p + n) (p + m) = p + max n m
apply add_max_distr_l. Qed.
n, m, p:positive

min (p + n) (p + m) = p + min n m
n, m, p:positive

min (p + n) (p + m) = p + min n m
n, m, p:positive

Proper (le ==> le) (add p)
n, m, p, x, x':positive

x <= x' -> p + x <= p + x'
apply add_le_mono_l. Qed.
n, m, p:positive

min (n + p) (m + p) = min n m + p
n, m, p:positive

min (n + p) (m + p) = min n m + p
n, m, p:positive

min (p + n) (p + m) = p + min n m
apply add_min_distr_l. Qed.
n, m, p:positive

max (p * n) (p * m) = p * max n m
n, m, p:positive

max (p * n) (p * m) = p * max n m
n, m, p:positive

Proper (le ==> le) (mul p)
n, m, p, x, x':positive

x <= x' -> p * x <= p * x'
apply mul_le_mono_l. Qed.
n, m, p:positive

max (n * p) (m * p) = max n m * p
n, m, p:positive

max (n * p) (m * p) = max n m * p
n, m, p:positive

max (p * n) (p * m) = p * max n m
apply mul_max_distr_l. Qed.
n, m, p:positive

min (p * n) (p * m) = p * min n m
n, m, p:positive

min (p * n) (p * m) = p * min n m
n, m, p:positive

Proper (le ==> le) (mul p)
n, m, p, x, x':positive

x <= x' -> p * x <= p * x'
apply mul_le_mono_l. Qed.
n, m, p:positive

min (n * p) (m * p) = min n m * p
n, m, p:positive

min (n * p) (m * p) = min n m * p
n, m, p:positive

min (p * n) (p * m) = p * min n m
apply mul_min_distr_l. Qed.

Results concerning iter_op


forall (A : Type) (op : A -> A -> A), (forall x y z : A, op x (op y z) = op (op x y) z) -> forall (p : positive) (a : A), iter_op op (succ p) a = op a (iter_op op p a)

forall (A : Type) (op : A -> A -> A), (forall x y z : A, op x (op y z) = op (op x y) z) -> forall (p : positive) (a : A), iter_op op (succ p) a = op a (iter_op op p a)
A:Type
op:A -> A -> A
H:forall x y z : A, op x (op y z) = op (op x y) z
p:positive
IHp:forall a0 : A, iter_op op (succ p) a0 = op a0 (iter_op op p a0)
a:A

iter_op op (succ p) (op a a) = op a (op a (iter_op op p (op a a)))
A:Type
op:A -> A -> A
H:forall x y z : A, op x (op y z) = op (op x y) z
p:positive
IHp:forall a0 : A, iter_op op (succ p) a0 = op a0 (iter_op op p a0)
a:A

iter_op op (succ p) (op a a) = op (op a a) (iter_op op p (op a a))
apply IHp. Qed.

Results about of_nat and of_succ_nat

n:nat

of_succ_nat n = of_nat (S n)
n:nat

of_succ_nat n = of_nat (S n)

of_succ_nat 0 = of_nat 1
n:nat
IHn:of_succ_nat n = of_nat (S n)
of_succ_nat (S n) = of_nat (S (S n))
n:nat
IHn:of_succ_nat n = of_nat (S n)

of_succ_nat (S n) = of_nat (S (S n))
n:nat
IHn:of_succ_nat n = of_nat (S n)

succ (of_succ_nat n) = succ match n with | 0%nat => 1 | S _ => succ (of_nat n) end
n:nat
IHn:of_succ_nat n = of_nat (S n)

of_succ_nat n = match n with | 0%nat => 1 | S _ => succ (of_nat n) end
now rewrite IHn. Qed.
n:nat

pred (of_succ_nat n) = of_nat n
n:nat

pred (of_succ_nat n) = of_nat n

pred (of_succ_nat 0) = of_nat 0
n:nat
pred (of_succ_nat (S n)) = of_nat (S n)
n:nat

pred (of_succ_nat (S n)) = of_nat (S n)
n:nat

pred (succ (of_succ_nat n)) = of_nat (S n)
n:nat

of_succ_nat n = of_nat (S n)
apply of_nat_succ. Qed.
n:nat

n <> 0%nat -> succ (of_nat n) = of_succ_nat n
n:nat

n <> 0%nat -> succ (of_nat n) = of_succ_nat n
n:nat

n <> 0%nat -> succ (of_nat n) = of_nat (S n)

0%nat <> 0%nat -> succ (of_nat 0) = of_nat 1
now destruct 1. Qed.

Correctness proofs for the square root function

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.

f, g:positive -> positive
p:(positive * mask)%type
x:positive

f = xO \/ f = xI -> g = xO \/ g = xI -> SqrtSpec p x -> SqrtSpec (sqrtrem_step f g p) (g (f x))
f, g:positive -> positive
p:(positive * mask)%type
x:positive

f = xO \/ f = xI -> g = xO \/ g = xI -> SqrtSpec p x -> SqrtSpec (sqrtrem_step f g p) (g (f x))
f, g:positive -> positive
p:(positive * mask)%type
x:positive
Hf:f = xO \/ f = xI
Hg:g = xO \/ g = xI
s:positive

SqrtSpec (sqrtrem_step f g (s, IsNul)) (g (f (s * s)))
f, g:positive -> positive
p:(positive * mask)%type
x:positive
Hf:f = xO \/ f = xI
Hg:g = xO \/ g = xI
s, r:positive
Hr:r <= s~0
SqrtSpec (sqrtrem_step f g (s, IsPos r)) (g (f (s * s + r)))
(* exact *)
f, g:positive -> positive
p:(positive * mask)%type
x:positive
Hf:f = xO \/ f = xI
Hg:g = xO \/ g = xI
s:positive

SqrtSpec (s~0, sub_mask (g (f 1)) 4) (g (f (s * s)))
f, g:positive -> positive
p:(positive * mask)%type
x:positive
Hf:f = xO \/ f = xI
Hg:g = xO \/ g = xI
s, r:positive
Hr:r <= s~0
SqrtSpec (sqrtrem_step f g (s, IsPos r)) (g (f (s * s + r)))
f, g:positive -> positive
p:(positive * mask)%type
x:positive
Hf:f = xO \/ f = xI
Hg:g = xO \/ g = xI
s, r:positive
Hr:r <= s~0

SqrtSpec (sqrtrem_step f g (s, IsPos r)) (g (f (s * s + r)))
(* approx *)
f, g:positive -> positive
p:(positive * mask)%type
x:positive
Hf:f = xO \/ f = xI
Hg:g = xO \/ g = xI
s, r:positive
Hr:r <= s~0
Hfg:forall p0 q : positive, g (f (p0 + q)) = p0~0~0 + g (f q)

SqrtSpec (sqrtrem_step f g (s, IsPos r)) (g (f (s * s + r)))
f, g:positive -> positive
p:(positive * mask)%type
x:positive
Hf:f = xO \/ f = xI
Hg:g = xO \/ g = xI
s, r:positive
Hr:r <= s~0
Hfg:forall p0 q : positive, g (f (p0 + q)) = p0~0~0 + g (f q)

SqrtSpec (if match s~0~1 ?= g (f r) with | Gt => false | _ => true end then (s~1, sub_mask (g (f r)) s~0~1) else (s~0, IsPos (g (f r)))) (g (f (s * s + r)))
f, g:positive -> positive
p:(positive * mask)%type
x:positive
Hf:f = xO \/ f = xI
Hg:g = xO \/ g = xI
s, r:positive
Hr:r <= s~0
Hfg:forall p0 q : positive, g (f (p0 + q)) = p0~0~0 + g (f q)
EQ:s~0~1 = g (f r)

SqrtSpec (s~1, sub_mask (g (f r)) s~0~1) (g (f (s * s + r)))
f, g:positive -> positive
p:(positive * mask)%type
x:positive
Hf:f = xO \/ f = xI
Hg:g = xO \/ g = xI
s, r:positive
Hr:r <= s~0
Hfg:forall p0 q : positive, g (f (p0 + q)) = p0~0~0 + g (f q)
LT:s~0~1 < g (f r)
SqrtSpec (s~1, sub_mask (g (f r)) s~0~1) (g (f (s * s + r)))
f, g:positive -> positive
p:(positive * mask)%type
x:positive
Hf:f = xO \/ f = xI
Hg:g = xO \/ g = xI
s, r:positive
Hr:r <= s~0
Hfg:forall p0 q : positive, g (f (p0 + q)) = p0~0~0 + g (f q)
GT:g (f r) < s~0~1
SqrtSpec (s~0, IsPos (g (f r))) (g (f (s * s + r)))
(* - EQ *)
f, g:positive -> positive
p:(positive * mask)%type
x:positive
Hf:f = xO \/ f = xI
Hg:g = xO \/ g = xI
s, r:positive
Hr:r <= s~0
Hfg:forall p0 q : positive, g (f (p0 + q)) = p0~0~0 + g (f q)
EQ:s~0~1 = g (f r)

SqrtSpec (s~1, IsNul) (g (f (s * s + r)))
f, g:positive -> positive
p:(positive * mask)%type
x:positive
Hf:f = xO \/ f = xI
Hg:g = xO \/ g = xI
s, r:positive
Hr:r <= s~0
Hfg:forall p0 q : positive, g (f (p0 + q)) = p0~0~0 + g (f q)
LT:s~0~1 < g (f r)
SqrtSpec (s~1, sub_mask (g (f r)) s~0~1) (g (f (s * s + r)))
f, g:positive -> positive
p:(positive * mask)%type
x:positive
Hf:f = xO \/ f = xI
Hg:g = xO \/ g = xI
s, r:positive
Hr:r <= s~0
Hfg:forall p0 q : positive, g (f (p0 + q)) = p0~0~0 + g (f q)
GT:g (f r) < s~0~1
SqrtSpec (s~0, IsPos (g (f r))) (g (f (s * s + r)))
f, g:positive -> positive
p:(positive * mask)%type
x:positive
Hf:f = xO \/ f = xI
Hg:g = xO \/ g = xI
s, r:positive
Hr:r <= s~0
Hfg:forall p0 q : positive, g (f (p0 + q)) = p0~0~0 + g (f q)
EQ:s~0~1 = g (f r)

g (f (s * s + r)) = s~1 * s~1
f, g:positive -> positive
p:(positive * mask)%type
x:positive
Hf:f = xO \/ f = xI
Hg:g = xO \/ g = xI
s, r:positive
Hr:r <= s~0
Hfg:forall p0 q : positive, g (f (p0 + q)) = p0~0~0 + g (f q)
LT:s~0~1 < g (f r)
SqrtSpec (s~1, sub_mask (g (f r)) s~0~1) (g (f (s * s + r)))
f, g:positive -> positive
p:(positive * mask)%type
x:positive
Hf:f = xO \/ f = xI
Hg:g = xO \/ g = xI
s, r:positive
Hr:r <= s~0
Hfg:forall p0 q : positive, g (f (p0 + q)) = p0~0~0 + g (f q)
GT:g (f r) < s~0~1
SqrtSpec (s~0, IsPos (g (f r))) (g (f (s * s + r)))
f:positive -> positive
p:(positive * mask)%type
x:positive
Hf:f = xO \/ f = xI
s, r:positive
Hr:r <= s~0
EQ:s~0 = f r
Hfg:forall p0 q : positive, (f (p0 + q))~1 = p0~0~0 + (f q)~1

(f (s * s + r))~1 = s~1 * s~1
f, g:positive -> positive
p:(positive * mask)%type
x:positive
Hf:f = xO \/ f = xI
Hg:g = xO \/ g = xI
s, r:positive
Hr:r <= s~0
Hfg:forall p0 q : positive, g (f (p0 + q)) = p0~0~0 + g (f q)
LT:s~0~1 < g (f r)
SqrtSpec (s~1, sub_mask (g (f r)) s~0~1) (g (f (s * s + r)))
f, g:positive -> positive
p:(positive * mask)%type
x:positive
Hf:f = xO \/ f = xI
Hg:g = xO \/ g = xI
s, r:positive
Hr:r <= s~0
Hfg:forall p0 q : positive, g (f (p0 + q)) = p0~0~0 + g (f q)
GT:g (f r) < s~0~1
SqrtSpec (s~0, IsPos (g (f r))) (g (f (s * s + r)))
p:(positive * mask)%type
x, s, r:positive
Hr:r <= s~0
Hfg:forall p0 q : positive, (p0 + q)~0~1 = p0~0~0 + q~0~1
EQ:s = r

(s * s + r)~0~1 = s~1 * s~1
f, g:positive -> positive
p:(positive * mask)%type
x:positive
Hf:f = xO \/ f = xI
Hg:g = xO \/ g = xI
s, r:positive
Hr:r <= s~0
Hfg:forall p0 q : positive, g (f (p0 + q)) = p0~0~0 + g (f q)
LT:s~0~1 < g (f r)
SqrtSpec (s~1, sub_mask (g (f r)) s~0~1) (g (f (s * s + r)))
f, g:positive -> positive
p:(positive * mask)%type
x:positive
Hf:f = xO \/ f = xI
Hg:g = xO \/ g = xI
s, r:positive
Hr:r <= s~0
Hfg:forall p0 q : positive, g (f (p0 + q)) = p0~0~0 + g (f q)
GT:g (f r) < s~0~1
SqrtSpec (s~0, IsPos (g (f r))) (g (f (s * s + r)))
p:(positive * mask)%type
x, r:positive
Hr:r <= r~0
Hfg:forall p0 q : positive, (p0 + q)~0~1 = p0~0~0 + q~0~1

(r * r + r)~0~1 = r~1 * r~1
f, g:positive -> positive
p:(positive * mask)%type
x:positive
Hf:f = xO \/ f = xI
Hg:g = xO \/ g = xI
s, r:positive
Hr:r <= s~0
Hfg:forall p0 q : positive, g (f (p0 + q)) = p0~0~0 + g (f q)
LT:s~0~1 < g (f r)
SqrtSpec (s~1, sub_mask (g (f r)) s~0~1) (g (f (s * s + r)))
f, g:positive -> positive
p:(positive * mask)%type
x:positive
Hf:f = xO \/ f = xI
Hg:g = xO \/ g = xI
s, r:positive
Hr:r <= s~0
Hfg:forall p0 q : positive, g (f (p0 + q)) = p0~0~0 + g (f q)
GT:g (f r) < s~0~1
SqrtSpec (s~0, IsPos (g (f r))) (g (f (s * s + r)))
f, g:positive -> positive
p:(positive * mask)%type
x:positive
Hf:f = xO \/ f = xI
Hg:g = xO \/ g = xI
s, r:positive
Hr:r <= s~0
Hfg:forall p0 q : positive, g (f (p0 + q)) = p0~0~0 + g (f q)
LT:s~0~1 < g (f r)

SqrtSpec (s~1, sub_mask (g (f r)) s~0~1) (g (f (s * s + r)))
f, g:positive -> positive
p:(positive * mask)%type
x:positive
Hf:f = xO \/ f = xI
Hg:g = xO \/ g = xI
s, r:positive
Hr:r <= s~0
Hfg:forall p0 q : positive, g (f (p0 + q)) = p0~0~0 + g (f q)
GT:g (f r) < s~0~1
SqrtSpec (s~0, IsPos (g (f r))) (g (f (s * s + r)))
(* - LT *)
f, g:positive -> positive
p:(positive * mask)%type
x:positive
Hf:f = xO \/ f = xI
Hg:g = xO \/ g = xI
s, r:positive
Hr:r <= s~0
Hfg:forall p0 q : positive, g (f (p0 + q)) = p0~0~0 + g (f q)
LT:s~0~1 < g (f r)
y:positive
H:s~0~1 + y = g (f r)

SqrtSpec (s~1, IsPos y) (g (f (s * s + r)))
f, g:positive -> positive
p:(positive * mask)%type
x:positive
Hf:f = xO \/ f = xI
Hg:g = xO \/ g = xI
s, r:positive
Hr:r <= s~0
Hfg:forall p0 q : positive, g (f (p0 + q)) = p0~0~0 + g (f q)
GT:g (f r) < s~0~1
SqrtSpec (s~0, IsPos (g (f r))) (g (f (s * s + r)))
f, g:positive -> positive
p:(positive * mask)%type
x:positive
Hf:f = xO \/ f = xI
Hg:g = xO \/ g = xI
s, r:positive
Hr:r <= s~0
Hfg:forall p0 q : positive, g (f (p0 + q)) = p0~0~0 + g (f q)
LT:s~0~1 < g (f r)
y:positive
H:s~0~1 + y = g (f r)

g (f (s * s + r)) = s~1 * s~1 + y
f, g:positive -> positive
p:(positive * mask)%type
x:positive
Hf:f = xO \/ f = xI
Hg:g = xO \/ g = xI
s, r:positive
Hr:r <= s~0
Hfg:forall p0 q : positive, g (f (p0 + q)) = p0~0~0 + g (f q)
LT:s~0~1 < g (f r)
y:positive
H:s~0~1 + y = g (f r)
y <= s~1~0
f, g:positive -> positive
p:(positive * mask)%type
x:positive
Hf:f = xO \/ f = xI
Hg:g = xO \/ g = xI
s, r:positive
Hr:r <= s~0
Hfg:forall p0 q : positive, g (f (p0 + q)) = p0~0~0 + g (f q)
GT:g (f r) < s~0~1
SqrtSpec (s~0, IsPos (g (f r))) (g (f (s * s + r)))
f, g:positive -> positive
p:(positive * mask)%type
x:positive
Hf:f = xO \/ f = xI
Hg:g = xO \/ g = xI
s, r:positive
Hr:r <= s~0
Hfg:forall p0 q : positive, g (f (p0 + q)) = p0~0~0 + g (f q)
LT:s~0~1 < g (f r)
y:positive
H:s~0~1 + y = g (f r)

(s * s)~0~0 + (s~0~1 + y) = s~1 * s~1 + y
f, g:positive -> positive
p:(positive * mask)%type
x:positive
Hf:f = xO \/ f = xI
Hg:g = xO \/ g = xI
s, r:positive
Hr:r <= s~0
Hfg:forall p0 q : positive, g (f (p0 + q)) = p0~0~0 + g (f q)
LT:s~0~1 < g (f r)
y:positive
H:s~0~1 + y = g (f r)
y <= s~1~0
f, g:positive -> positive
p:(positive * mask)%type
x:positive
Hf:f = xO \/ f = xI
Hg:g = xO \/ g = xI
s, r:positive
Hr:r <= s~0
Hfg:forall p0 q : positive, g (f (p0 + q)) = p0~0~0 + g (f q)
GT:g (f r) < s~0~1
SqrtSpec (s~0, IsPos (g (f r))) (g (f (s * s + r)))
f, g:positive -> positive
p:(positive * mask)%type
x:positive
Hf:f = xO \/ f = xI
Hg:g = xO \/ g = xI
s, r:positive
Hr:r <= s~0
Hfg:forall p0 q : positive, g (f (p0 + q)) = p0~0~0 + g (f q)
LT:s~0~1 < g (f r)
y:positive
H:s~0~1 + y = g (f r)

y <= s~1~0
f, g:positive -> positive
p:(positive * mask)%type
x:positive
Hf:f = xO \/ f = xI
Hg:g = xO \/ g = xI
s, r:positive
Hr:r <= s~0
Hfg:forall p0 q : positive, g (f (p0 + q)) = p0~0~0 + g (f q)
GT:g (f r) < s~0~1
SqrtSpec (s~0, IsPos (g (f r))) (g (f (s * s + r)))
f, g:positive -> positive
p:(positive * mask)%type
x:positive
Hf:f = xO \/ f = xI
Hg:g = xO \/ g = xI
s, r:positive
Hr:r <= s~0
LT:s~0~1 < g (f r)
y:positive
H:s~0~1 + y = g (f r)

y <= s~1~0
f, g:positive -> positive
p:(positive * mask)%type
x:positive
Hf:f = xO \/ f = xI
Hg:g = xO \/ g = xI
s, r:positive
Hr:r <= s~0
Hfg:forall p0 q : positive, g (f (p0 + q)) = p0~0~0 + g (f q)
GT:g (f r) < s~0~1
SqrtSpec (s~0, IsPos (g (f r))) (g (f (s * s + r)))
f, g:positive -> positive
p:(positive * mask)%type
x:positive
Hf:f = xO \/ f = xI
Hg:g = xO \/ g = xI
s, r:positive
Hr:r < succ s~0
LT:s~0~1 < g (f r)
y:positive
H:s~0~1 + y = g (f r)

y <= s~1~0
f, g:positive -> positive
p:(positive * mask)%type
x:positive
Hf:f = xO \/ f = xI
Hg:g = xO \/ g = xI
s, r:positive
Hr:r <= s~0
Hfg:forall p0 q : positive, g (f (p0 + q)) = p0~0~0 + g (f q)
GT:g (f r) < s~0~1
SqrtSpec (s~0, IsPos (g (f r))) (g (f (s * s + r)))
f, g:positive -> positive
p:(positive * mask)%type
x:positive
Hf:f = xO \/ f = xI
Hg:g = xO \/ g = xI
s, r:positive
Hr:r < s~1
LT:s~0~1 < g (f r)
y:positive
H:s~0~1 + y = g (f r)

y <= s~1~0
f, g:positive -> positive
p:(positive * mask)%type
x:positive
Hf:f = xO \/ f = xI
Hg:g = xO \/ g = xI
s, r:positive
Hr:r <= s~0
Hfg:forall p0 q : positive, g (f (p0 + q)) = p0~0~0 + g (f q)
GT:g (f r) < s~0~1
SqrtSpec (s~0, IsPos (g (f r))) (g (f (s * s + r)))
f, g:positive -> positive
p:(positive * mask)%type
x:positive
Hf:f = xO \/ f = xI
Hg:g = xO \/ g = xI
s, r:positive
Hr:r < s~1
LT:s~0~1 < g (f r)
y:positive
H:s~0~1 + y = g (f r)

g (f r) < s~0~1 + succ s~1~0
f, g:positive -> positive
p:(positive * mask)%type
x:positive
Hf:f = xO \/ f = xI
Hg:g = xO \/ g = xI
s, r:positive
Hr:r <= s~0
Hfg:forall p0 q : positive, g (f (p0 + q)) = p0~0~0 + g (f q)
GT:g (f r) < s~0~1
SqrtSpec (s~0, IsPos (g (f r))) (g (f (s * s + r)))
f, g:positive -> positive
p:(positive * mask)%type
x:positive
Hf:f = xO \/ f = xI
Hg:g = xO \/ g = xI
s, r:positive
Hr:r < s~1
LT:s~0~1 < g (f r)
y:positive
H:s~0~1 + y = g (f r)

g (f r) < (add_carry s s)~0~0
f, g:positive -> positive
p:(positive * mask)%type
x:positive
Hf:f = xO \/ f = xI
Hg:g = xO \/ g = xI
s, r:positive
Hr:r <= s~0
Hfg:forall p0 q : positive, g (f (p0 + q)) = p0~0~0 + g (f q)
GT:g (f r) < s~0~1
SqrtSpec (s~0, IsPos (g (f r))) (g (f (s * s + r)))
f, g:positive -> positive
p:(positive * mask)%type
x:positive
Hf:f = xO \/ f = xI
Hg:g = xO \/ g = xI
s, r:positive
Hr:r < s~1
LT:s~0~1 < g (f r)
y:positive
H:s~0~1 + y = g (f r)

g (f r) < (succ s~0)~0~0
f, g:positive -> positive
p:(positive * mask)%type
x:positive
Hf:f = xO \/ f = xI
Hg:g = xO \/ g = xI
s, r:positive
Hr:r <= s~0
Hfg:forall p0 q : positive, g (f (p0 + q)) = p0~0~0 + g (f q)
GT:g (f r) < s~0~1
SqrtSpec (s~0, IsPos (g (f r))) (g (f (s * s + r)))
f, g:positive -> positive
p:(positive * mask)%type
x:positive
Hf:f = xO \/ f = xI
Hg:g = xO \/ g = xI
s, r:positive
Hr:r < s~1
LT:s~0~1 < g (f r)
y:positive
H:s~0~1 + y = g (f r)

g (f r) < s~1~0~0
f, g:positive -> positive
p:(positive * mask)%type
x:positive
Hf:f = xO \/ f = xI
Hg:g = xO \/ g = xI
s, r:positive
Hr:r <= s~0
Hfg:forall p0 q : positive, g (f (p0 + q)) = p0~0~0 + g (f q)
GT:g (f r) < s~0~1
SqrtSpec (s~0, IsPos (g (f r))) (g (f (s * s + r)))
f, g:positive -> positive
p:(positive * mask)%type
x:positive
Hf:f = xO \/ f = xI
Hg:g = xO \/ g = xI
s, r:positive
Hr:r <= s~0
Hfg:forall p0 q : positive, g (f (p0 + q)) = p0~0~0 + g (f q)
GT:g (f r) < s~0~1

SqrtSpec (s~0, IsPos (g (f r))) (g (f (s * s + r)))
(* - GT *)
f, g:positive -> positive
p:(positive * mask)%type
x:positive
Hf:f = xO \/ f = xI
Hg:g = xO \/ g = xI
s, r:positive
Hr:r <= s~0
Hfg:forall p0 q : positive, g (f (p0 + q)) = p0~0~0 + g (f q)
GT:g (f r) < s~0~1

g (f (s * s + r)) = s~0 * s~0 + g (f r)
f, g:positive -> positive
p:(positive * mask)%type
x:positive
Hf:f = xO \/ f = xI
Hg:g = xO \/ g = xI
s, r:positive
Hr:r <= s~0
Hfg:forall p0 q : positive, g (f (p0 + q)) = p0~0~0 + g (f q)
GT:g (f r) < s~0~1
g (f r) <= s~0~0
f, g:positive -> positive
p:(positive * mask)%type
x:positive
Hf:f = xO \/ f = xI
Hg:g = xO \/ g = xI
s, r:positive
Hr:r <= s~0
Hfg:forall p0 q : positive, g (f (p0 + q)) = p0~0~0 + g (f q)
GT:g (f r) < s~0~1

g (f r) <= s~0~0
apply lt_succ_r, GT. Qed.
p:positive

SqrtSpec (sqrtrem p) p
p:positive

SqrtSpec (sqrtrem p) p

forall p : positive, SqrtSpec (sqrtrem p) p
sqrtrem_spec:forall p : positive, SqrtSpec (sqrtrem p) p

forall p : positive, SqrtSpec (sqrtrem p) p
destruct p; try destruct p; try (constructor; easy); apply sqrtrem_step_spec; auto. Qed.
p:positive

let s := sqrt p in s * s <= p < succ s * succ s
p:positive

let s := sqrt p in s * s <= p < succ s * succ s
p:positive

sqrt p * sqrt p <= p < succ (sqrt p) * succ (sqrt p)
p:positive
H:SqrtSpec (sqrtrem p) p

sqrt p * sqrt p <= p < succ (sqrt p) * succ (sqrt p)
p:positive
H:SqrtSpec (sqrtrem p) p

fst (sqrtrem p) * fst (sqrtrem p) <= p < succ (fst (sqrtrem p)) * succ (fst (sqrtrem p))
p, s:positive
rm:mask
H:SqrtSpec (s, rm) p

s * s <= p < succ s * succ s
s:positive
rm:mask

s * s <= s * s < succ s * succ s
s:positive
rm:mask
r:positive
H1:r <= s~0
s * s <= s * s + r < succ s * succ s
(* exact *)
s:positive
rm:mask

s * s <= s * s
s:positive
rm:mask
s * s < succ s * succ s
s:positive
rm:mask
r:positive
H1:r <= s~0
s * s <= s * s + r < succ s * succ s
s:positive
rm:mask

s * s < succ s * succ s
s:positive
rm:mask
r:positive
H1:r <= s~0
s * s <= s * s + r < succ s * succ s
s:positive
rm:mask
r:positive
H1:r <= s~0

s * s <= s * s + r < succ s * succ s
(* approx *)
s:positive
rm:mask
r:positive
H1:r <= s~0

s * s <= s * s + r
s:positive
rm:mask
r:positive
H1:r <= s~0
s * s + r < succ s * succ s
s:positive
rm:mask
r:positive
H1:r <= s~0

s * s + r < succ s * succ s
s:positive
rm:mask
r:positive
H1:r <= s~0

s * s + r < 1 + s + (s + s * s)
s:positive
rm:mask
r:positive
H1:r <= s~0

r + s * s < 1 + s + s + s * s
s:positive
rm:mask
r:positive
H1:r <= s~0

r < 1 + s + s
now rewrite <- add_assoc, add_diag, add_1_l, lt_succ_r. Qed.

Correctness proofs for the gcd function

p, q, r:positive

(p | r) -> (p | q + r) -> (p | q)
p, q, r:positive

(p | r) -> (p | q + r) -> (p | q)
p, q, r, s:positive
Hs:r = s * p
t:positive
Ht:q + r = t * p

(p | q)
p, q, r, s:positive
Hs:r = s * p
t:positive
Ht:q + r = t * p

q = (t - s) * p
p, q, r, s:positive
Hs:r = s * p
t:positive
Ht:q + r = t * p

q = t * p - s * p
p, q, r, s:positive
Hs:r = s * p
t:positive
Ht:q + r = t * p
s < t
p, q, r, s:positive
Hs:r = s * p
t:positive
Ht:q + r = t * p

q = q + r - r
p, q, r, s:positive
Hs:r = s * p
t:positive
Ht:q + r = t * p
s < t
p, q, r, s:positive
Hs:r = s * p
t:positive
Ht:q + r = t * p

q + r - r = q
p, q, r, s:positive
Hs:r = s * p
t:positive
Ht:q + r = t * p
s < t
p, q, r, s:positive
Hs:r = s * p
t:positive
Ht:q + r = t * p

s < t
p, q, r, s:positive
Hs:r = s * p
t:positive
Ht:q + r = t * p

s * p < t * p
p, q, r, s:positive
Hs:r = s * p
t:positive
Ht:q + r = t * p

r < r + q
apply lt_add_r. Qed.
p, q, r:positive

(p | q~0) -> (p | r~1) -> (p | q)
p, q, r:positive

(p | q~0) -> (p | r~1) -> (p | q)
p, q, r, s:positive
Hs:q~0 = s * p
t:positive
Ht:r~1 = t * p

(p | q)
p, q, r, s:positive
Hs:q~0 = s * p~1
t:positive
Ht:r~1 = t * p~1

(p~1 | q)
p, q, r, s:positive
Hs:q~0 = s * p~0
t:positive
Ht:r~1 = t * p~0
(p~0 | q)
q, r, s:positive
Hs:q~0 = s * 1
t:positive
Ht:r~1 = t * 1
(1 | q)
p, q, r, s:positive
Hs:q~0 = s~0 * p~1
t:positive
Ht:r~1 = t * p~1

(p~1 | q)
p, q, r, s:positive
Hs:q~0 = s * p~0
t:positive
Ht:r~1 = t * p~0
(p~0 | q)
q, r, s:positive
Hs:q~0 = s * 1
t:positive
Ht:r~1 = t * 1
(1 | q)
p, q, r, s:positive
Hs:q~0 = (s * p~1)~0
t:positive
Ht:r~1 = t * p~1

(p~1 | q)
p, q, r, s:positive
Hs:q~0 = s * p~0
t:positive
Ht:r~1 = t * p~0
(p~0 | q)
q, r, s:positive
Hs:q~0 = s * 1
t:positive
Ht:r~1 = t * 1
(1 | q)
p, q, r, s:positive
Hs:q = s * p~1
t:positive
Ht:r~1 = t * p~1

(p~1 | q)
p, q, r, s:positive
Hs:q~0 = s * p~0
t:positive
Ht:r~1 = t * p~0
(p~0 | q)
q, r, s:positive
Hs:q~0 = s * 1
t:positive
Ht:r~1 = t * 1
(1 | q)
p, q, r, s:positive
Hs:q~0 = s * p~0
t:positive
Ht:r~1 = t * p~0

(p~0 | q)
q, r, s:positive
Hs:q~0 = s * 1
t:positive
Ht:r~1 = t * 1
(1 | q)
q, r, s:positive
Hs:q~0 = s * 1
t:positive
Ht:r~1 = t * 1

(1 | q)
exists q; now rewrite mul_1_r. Qed.
p, q:positive

(p~0 | q~0) <-> (p | q)
p, q:positive

(p~0 | q~0) <-> (p | q)
p, q, r:positive
H:q~0 = r * p~0

(p | q)
p, q, r:positive
H:q = r * p
(p~0 | q~0)
p, q, r:positive
H:q~0 = (r * p)~0

(p | q)
p, q, r:positive
H:q = r * p
(p~0 | q~0)
p, q, r:positive
H:q = r * p

(p | q)
p, q, r:positive
H:q = r * p
(p~0 | q~0)
p, q, r:positive
H:q = r * p

(p~0 | q~0)
p, q, r:positive
H:q = r * p

q~0 = r * p~0
p, q, r:positive
H:q = r * p

q~0 = (r * p)~0
f_equal; auto. Qed.
p, q, r:positive

(p | q) -> (p | q * r)
p, q, r:positive

(p | q) -> (p | q * r)
p, q, r, s:positive
H:q = s * p

(p | q * r)
p, q, r, s:positive
H:q = s * p

q * r = s * r * p
p, q, r, s:positive
H:q = s * p

q * r = s * p * r
now f_equal. Qed.
p, q, r:positive

(p | r) -> (p | q * r)
p, q, r:positive

(p | r) -> (p | q * r)
p, q, r:positive

(p | r) -> (p | r * q)
apply divide_mul_l. Qed.
The first component of ggcd is gcd

forall (n : nat) (a b : positive), fst (ggcdn n a b) = gcdn n a b

forall (n : nat) (a b : positive), fst (ggcdn n a b) = gcdn n a b

forall a b : positive, fst (ggcdn 0 a b) = gcdn 0 a b
n:nat
IHn:forall a b : positive, fst (ggcdn n a b) = gcdn n a b
forall a b : positive, fst (ggcdn (S n) a b) = gcdn (S n) a b
n:nat
IHn:forall a b : positive, fst (ggcdn n a b) = gcdn n a b

forall a b : positive, fst (ggcdn (S n) a b) = gcdn (S n) a b
destruct a, b; simpl; auto; try case compare_spec; simpl; trivial; rewrite <- IHn; destruct ggcdn as (g,(u,v)); simpl; auto. Qed.

forall a b : positive, fst (ggcd a b) = gcd a b

forall a b : positive, fst (ggcd a b) = gcd a b

forall a b : positive, fst (ggcdn (size_nat a + size_nat b) a b) = gcdn (size_nat a + size_nat b) a b
a, b:positive

fst (ggcdn (size_nat a + size_nat b) a b) = gcdn (size_nat a + size_nat b) a b
apply ggcdn_gcdn. Qed.
The other components of ggcd are indeed the correct factors.
Ltac destr_pggcdn IHn :=
 match goal with |- context [ ggcdn _ ?x ?y ] =>
  generalize (IHn x y); destruct ggcdn as (g,(u,v)); simpl
 end.


forall (n : nat) (a b : positive), let '(g, (aa, bb)) := ggcdn n a b in a = g * aa /\ b = g * bb

forall (n : nat) (a b : positive), let '(g, (aa, bb)) := ggcdn n a b in a = g * aa /\ b = g * bb

forall a b : positive, let '(g, (aa, bb)) := ggcdn 0 a b in a = g * aa /\ b = g * bb
n:nat
IHn:forall a b : positive, let '(g, (aa, bb)) := ggcdn n a b in a = g * aa /\ b = g * bb
forall a b : positive, let '(g, (aa, bb)) := ggcdn (S n) a b in a = g * aa /\ b = g * bb
n:nat
IHn:forall a b : positive, let '(g, (aa, bb)) := ggcdn n a b in a = g * aa /\ b = g * bb

forall a b : positive, let '(g, (aa, bb)) := ggcdn (S n) a b in a = g * aa /\ b = g * bb
n:nat
IHn:forall a0 b0 : positive, let '(g, (aa, bb)) := ggcdn n a0 b0 in a0 = g * aa /\ b0 = g * bb
a, b:positive

a = b -> a~1 = a~1 * 1 /\ b~1 = a~1 * 1
n:nat
IHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bb
a, b, g, u, v:positive
b - a = g * u /\ a~1 = g * v -> a < b -> a~1 = g * v /\ b~1 = g * (v + u~0)
n:nat
IHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bb
a, b, g, u, v:positive
a - b = g * u /\ b~1 = g * v -> b < a -> a~1 = g * (v + u~0) /\ b~1 = g * v
n:nat
IHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bb
a, b, g, u, v:positive
a~1 = g * u /\ b = g * v -> a~1 = g * u /\ b~0 = g * v~0
n:nat
IHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bb
a, b, g, u, v:positive
a = g * u /\ b~1 = g * v -> a~0 = g * u~0 /\ b~1 = g * v
n:nat
IHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bb
a, b, g, u, v:positive
a = g * u /\ b = g * v -> a~0 = (g * u)~0 /\ b~0 = (g * v)~0
(* Eq *)
n:nat
IHn:forall a b0 : positive, let '(g, (aa, bb)) := ggcdn n a b0 in a = g * aa /\ b0 = g * bb
b:positive

b~1 = b~1 * 1 /\ b~1 = b~1 * 1
n:nat
IHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bb
a, b, g, u, v:positive
b - a = g * u /\ a~1 = g * v -> a < b -> a~1 = g * v /\ b~1 = g * (v + u~0)
n:nat
IHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bb
a, b, g, u, v:positive
a - b = g * u /\ b~1 = g * v -> b < a -> a~1 = g * (v + u~0) /\ b~1 = g * v
n:nat
IHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bb
a, b, g, u, v:positive
a~1 = g * u /\ b = g * v -> a~1 = g * u /\ b~0 = g * v~0
n:nat
IHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bb
a, b, g, u, v:positive
a = g * u /\ b~1 = g * v -> a~0 = g * u~0 /\ b~1 = g * v
n:nat
IHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bb
a, b, g, u, v:positive
a = g * u /\ b = g * v -> a~0 = (g * u)~0 /\ b~0 = (g * v)~0
n:nat
IHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bb
a, b, g, u, v:positive

b - a = g * u /\ a~1 = g * v -> a < b -> a~1 = g * v /\ b~1 = g * (v + u~0)
n:nat
IHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bb
a, b, g, u, v:positive
a - b = g * u /\ b~1 = g * v -> b < a -> a~1 = g * (v + u~0) /\ b~1 = g * v
n:nat
IHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bb
a, b, g, u, v:positive
a~1 = g * u /\ b = g * v -> a~1 = g * u /\ b~0 = g * v~0
n:nat
IHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bb
a, b, g, u, v:positive
a = g * u /\ b~1 = g * v -> a~0 = g * u~0 /\ b~1 = g * v
n:nat
IHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bb
a, b, g, u, v:positive
a = g * u /\ b = g * v -> a~0 = (g * u)~0 /\ b~0 = (g * v)~0
(* Lt *)
n:nat
IHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bb
a, b, g, u, v:positive
H':b - a = g * u
H:a~1 = g * v
LT:a < b

b~1 = g * (v + u~0)
n:nat
IHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bb
a, b, g, u, v:positive
a - b = g * u /\ b~1 = g * v -> b < a -> a~1 = g * (v + u~0) /\ b~1 = g * v
n:nat
IHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bb
a, b, g, u, v:positive
a~1 = g * u /\ b = g * v -> a~1 = g * u /\ b~0 = g * v~0
n:nat
IHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bb
a, b, g, u, v:positive
a = g * u /\ b~1 = g * v -> a~0 = g * u~0 /\ b~1 = g * v
n:nat
IHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bb
a, b, g, u, v:positive
a = g * u /\ b = g * v -> a~0 = (g * u)~0 /\ b~0 = (g * v)~0
n:nat
IHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bb
a, b, g, u, v:positive
H':b - a = g * u
H:a~1 = g * v
LT:a < b

b~1 = a~1 + (b - a)~0
n:nat
IHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bb
a, b, g, u, v:positive
a - b = g * u /\ b~1 = g * v -> b < a -> a~1 = g * (v + u~0) /\ b~1 = g * v
n:nat
IHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bb
a, b, g, u, v:positive
a~1 = g * u /\ b = g * v -> a~1 = g * u /\ b~0 = g * v~0
n:nat
IHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bb
a, b, g, u, v:positive
a = g * u /\ b~1 = g * v -> a~0 = g * u~0 /\ b~1 = g * v
n:nat
IHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bb
a, b, g, u, v:positive
a = g * u /\ b = g * v -> a~0 = (g * u)~0 /\ b~0 = (g * v)~0
n:nat
IHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bb
a, b, g, u, v:positive
H':b - a = g * u
H:a~1 = g * v
LT:a < b

b~1 = (a + (b - a))~1
n:nat
IHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bb
a, b, g, u, v:positive
a - b = g * u /\ b~1 = g * v -> b < a -> a~1 = g * (v + u~0) /\ b~1 = g * v
n:nat
IHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bb
a, b, g, u, v:positive
a~1 = g * u /\ b = g * v -> a~1 = g * u /\ b~0 = g * v~0
n:nat
IHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bb
a, b, g, u, v:positive
a = g * u /\ b~1 = g * v -> a~0 = g * u~0 /\ b~1 = g * v
n:nat
IHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bb
a, b, g, u, v:positive
a = g * u /\ b = g * v -> a~0 = (g * u)~0 /\ b~0 = (g * v)~0
n:nat
IHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bb
a, b, g, u, v:positive
H':b - a = g * u
H:a~1 = g * v
LT:a < b

b = a + (b - a)
n:nat
IHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bb
a, b, g, u, v:positive
a - b = g * u /\ b~1 = g * v -> b < a -> a~1 = g * (v + u~0) /\ b~1 = g * v
n:nat
IHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bb
a, b, g, u, v:positive
a~1 = g * u /\ b = g * v -> a~1 = g * u /\ b~0 = g * v~0
n:nat
IHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bb
a, b, g, u, v:positive
a = g * u /\ b~1 = g * v -> a~0 = g * u~0 /\ b~1 = g * v
n:nat
IHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bb
a, b, g, u, v:positive
a = g * u /\ b = g * v -> a~0 = (g * u)~0 /\ b~0 = (g * v)~0
n:nat
IHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bb
a, b, g, u, v:positive
H':b - a = g * u
H:a~1 = g * v
LT:a < b

a + (b - a) = b
n:nat
IHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bb
a, b, g, u, v:positive
a - b = g * u /\ b~1 = g * v -> b < a -> a~1 = g * (v + u~0) /\ b~1 = g * v
n:nat
IHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bb
a, b, g, u, v:positive
a~1 = g * u /\ b = g * v -> a~1 = g * u /\ b~0 = g * v~0
n:nat
IHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bb
a, b, g, u, v:positive
a = g * u /\ b~1 = g * v -> a~0 = g * u~0 /\ b~1 = g * v
n:nat
IHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bb
a, b, g, u, v:positive
a = g * u /\ b = g * v -> a~0 = (g * u)~0 /\ b~0 = (g * v)~0
n:nat
IHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bb
a, b, g, u, v:positive
H':b - a = g * u
H:a~1 = g * v
LT:a < b

b - a + a = b
n:nat
IHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bb
a, b, g, u, v:positive
a - b = g * u /\ b~1 = g * v -> b < a -> a~1 = g * (v + u~0) /\ b~1 = g * v
n:nat
IHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bb
a, b, g, u, v:positive
a~1 = g * u /\ b = g * v -> a~1 = g * u /\ b~0 = g * v~0
n:nat
IHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bb
a, b, g, u, v:positive
a = g * u /\ b~1 = g * v -> a~0 = g * u~0 /\ b~1 = g * v
n:nat
IHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bb
a, b, g, u, v:positive
a = g * u /\ b = g * v -> a~0 = (g * u)~0 /\ b~0 = (g * v)~0
n:nat
IHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bb
a, b, g, u, v:positive

a - b = g * u /\ b~1 = g * v -> b < a -> a~1 = g * (v + u~0) /\ b~1 = g * v
n:nat
IHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bb
a, b, g, u, v:positive
a~1 = g * u /\ b = g * v -> a~1 = g * u /\ b~0 = g * v~0
n:nat
IHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bb
a, b, g, u, v:positive
a = g * u /\ b~1 = g * v -> a~0 = g * u~0 /\ b~1 = g * v
n:nat
IHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bb
a, b, g, u, v:positive
a = g * u /\ b = g * v -> a~0 = (g * u)~0 /\ b~0 = (g * v)~0
(* Gt *)
n:nat
IHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bb
a, b, g, u, v:positive
H':a - b = g * u
H:b~1 = g * v
LT:b < a

a~1 = g * (v + u~0)
n:nat
IHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bb
a, b, g, u, v:positive
a~1 = g * u /\ b = g * v -> a~1 = g * u /\ b~0 = g * v~0
n:nat
IHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bb
a, b, g, u, v:positive
a = g * u /\ b~1 = g * v -> a~0 = g * u~0 /\ b~1 = g * v
n:nat
IHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bb
a, b, g, u, v:positive
a = g * u /\ b = g * v -> a~0 = (g * u)~0 /\ b~0 = (g * v)~0
n:nat
IHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bb
a, b, g, u, v:positive
H':a - b = g * u
H:b~1 = g * v
LT:b < a

a~1 = b~1 + (a - b)~0
n:nat
IHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bb
a, b, g, u, v:positive
a~1 = g * u /\ b = g * v -> a~1 = g * u /\ b~0 = g * v~0
n:nat
IHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bb
a, b, g, u, v:positive
a = g * u /\ b~1 = g * v -> a~0 = g * u~0 /\ b~1 = g * v
n:nat
IHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bb
a, b, g, u, v:positive
a = g * u /\ b = g * v -> a~0 = (g * u)~0 /\ b~0 = (g * v)~0
n:nat
IHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bb
a, b, g, u, v:positive
H':a - b = g * u
H:b~1 = g * v
LT:b < a

a~1 = (b + (a - b))~1
n:nat
IHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bb
a, b, g, u, v:positive
a~1 = g * u /\ b = g * v -> a~1 = g * u /\ b~0 = g * v~0
n:nat
IHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bb
a, b, g, u, v:positive
a = g * u /\ b~1 = g * v -> a~0 = g * u~0 /\ b~1 = g * v
n:nat
IHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bb
a, b, g, u, v:positive
a = g * u /\ b = g * v -> a~0 = (g * u)~0 /\ b~0 = (g * v)~0
n:nat
IHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bb
a, b, g, u, v:positive
H':a - b = g * u
H:b~1 = g * v
LT:b < a

a = b + (a - b)
n:nat
IHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bb
a, b, g, u, v:positive
a~1 = g * u /\ b = g * v -> a~1 = g * u /\ b~0 = g * v~0
n:nat
IHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bb
a, b, g, u, v:positive
a = g * u /\ b~1 = g * v -> a~0 = g * u~0 /\ b~1 = g * v
n:nat
IHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bb
a, b, g, u, v:positive
a = g * u /\ b = g * v -> a~0 = (g * u)~0 /\ b~0 = (g * v)~0
n:nat
IHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bb
a, b, g, u, v:positive
H':a - b = g * u
H:b~1 = g * v
LT:b < a

b + (a - b) = a
n:nat
IHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bb
a, b, g, u, v:positive
a~1 = g * u /\ b = g * v -> a~1 = g * u /\ b~0 = g * v~0
n:nat
IHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bb
a, b, g, u, v:positive
a = g * u /\ b~1 = g * v -> a~0 = g * u~0 /\ b~1 = g * v
n:nat
IHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bb
a, b, g, u, v:positive
a = g * u /\ b = g * v -> a~0 = (g * u)~0 /\ b~0 = (g * v)~0
n:nat
IHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bb
a, b, g, u, v:positive
H':a - b = g * u
H:b~1 = g * v
LT:b < a

a - b + b = a
n:nat
IHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bb
a, b, g, u, v:positive
a~1 = g * u /\ b = g * v -> a~1 = g * u /\ b~0 = g * v~0
n:nat
IHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bb
a, b, g, u, v:positive
a = g * u /\ b~1 = g * v -> a~0 = g * u~0 /\ b~1 = g * v
n:nat
IHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bb
a, b, g, u, v:positive
a = g * u /\ b = g * v -> a~0 = (g * u)~0 /\ b~0 = (g * v)~0
n:nat
IHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bb
a, b, g, u, v:positive

a~1 = g * u /\ b = g * v -> a~1 = g * u /\ b~0 = g * v~0
n:nat
IHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bb
a, b, g, u, v:positive
a = g * u /\ b~1 = g * v -> a~0 = g * u~0 /\ b~1 = g * v
n:nat
IHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bb
a, b, g, u, v:positive
a = g * u /\ b = g * v -> a~0 = (g * u)~0 /\ b~0 = (g * v)~0
(* Then... *)
n:nat
IHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bb
a, b, g, u, v:positive
H:a~1 = g * u
H':b = g * v

b~0 = g * v~0
n:nat
IHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bb
a, b, g, u, v:positive
a = g * u /\ b~1 = g * v -> a~0 = g * u~0 /\ b~1 = g * v
n:nat
IHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bb
a, b, g, u, v:positive
a = g * u /\ b = g * v -> a~0 = (g * u)~0 /\ b~0 = (g * v)~0
n:nat
IHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bb
a, b, g, u, v:positive

a = g * u /\ b~1 = g * v -> a~0 = g * u~0 /\ b~1 = g * v
n:nat
IHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bb
a, b, g, u, v:positive
a = g * u /\ b = g * v -> a~0 = (g * u)~0 /\ b~0 = (g * v)~0
n:nat
IHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bb
a, b, g, u, v:positive
H:a = g * u
H':b~1 = g * v

a~0 = g * u~0
n:nat
IHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bb
a, b, g, u, v:positive
a = g * u /\ b = g * v -> a~0 = (g * u)~0 /\ b~0 = (g * v)~0
n:nat
IHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bb
a, b, g, u, v:positive

a = g * u /\ b = g * v -> a~0 = (g * u)~0 /\ b~0 = (g * v)~0
intros (H,H'); split; subst; auto. Qed.

forall a b : positive, let '(g, (aa, bb)) := ggcd a b in a = g * aa /\ b = g * bb

forall a b : positive, let '(g, (aa, bb)) := ggcd a b in a = g * aa /\ b = g * bb

forall a b : positive, let '(g, (aa, bb)) := ggcdn (size_nat a + size_nat b) a b in a = g * aa /\ b = g * bb
a, b:positive

let '(g, (aa, bb)) := ggcdn (size_nat a + size_nat b) a b in a = g * aa /\ b = g * bb
apply ggcdn_correct_divisors. Qed.
We can use this fact to prove a part of the gcd correctness

forall a b : positive, (gcd a b | a)

forall a b : positive, (gcd a b | a)
a, b:positive

(gcd a b | a)
a, b:positive

(fst (ggcd a b) | a)
a, b:positive

(let '(g, (aa, bb)) := ggcd a b in a = g * aa /\ b = g * bb) -> (fst (ggcd a b) | a)
a, b, g, aa, bb:positive

a = g * aa /\ b = g * bb -> (g | a)
a, b, g, aa, bb:positive
H:a = g * aa

(g | a)
a, b, g, aa, bb:positive
H:a = g * aa

a = aa * g
now rewrite mul_comm. Qed.

forall a b : positive, (gcd a b | b)

forall a b : positive, (gcd a b | b)
a, b:positive

(gcd a b | b)
a, b:positive

(fst (ggcd a b) | b)
a, b:positive

(let '(g, (aa, bb)) := ggcd a b in a = g * aa /\ b = g * bb) -> (fst (ggcd a b) | b)
a, b, g, aa, bb:positive

a = g * aa /\ b = g * bb -> (g | b)
a, b, g, aa, bb:positive
H:b = g * bb

(g | b)
a, b, g, aa, bb:positive
H:b = g * bb

b = bb * g
now rewrite mul_comm. Qed.
We now prove directly that gcd is the greatest amongst common divisors

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

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

forall a b : positive, (size_nat a + size_nat b <= 0)%nat -> forall p : positive, (p | a) -> (p | b) -> (p | gcdn 0 a b)
n:nat
IHn:forall a b : positive, (size_nat a + size_nat b <= n)%nat -> forall p : positive, (p | a) -> (p | b) -> (p | gcdn n a b)
forall a b : positive, (size_nat a + size_nat b <= S n)%nat -> forall p : positive, (p | a) -> (p | b) -> (p | gcdn (S n) a b)
n:nat
IHn:forall a b : positive, (size_nat a + size_nat b <= n)%nat -> forall p : positive, (p | a) -> (p | b) -> (p | gcdn n a b)

forall a b : positive, (size_nat a + size_nat b <= S n)%nat -> forall p : positive, (p | a) -> (p | b) -> (p | gcdn (S n) a b)
n:nat
IHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)
a, b:positive

a < b -> (S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~1) -> (p | b~1) -> (p | gcdn n (b - a) a~1)
n:nat
IHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)
a, b:positive
b < a -> (S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~1) -> (p | b~1) -> (p | gcdn n (a - b) b~1)
n:nat
IHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)
a, b:positive
(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~1) -> (p | b~0) -> (p | gcdn n a~1 b)
n:nat
IHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)
a, b:positive
(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~0) -> (p | b~1) -> (p | gcdn n a b~1)
n:nat
IHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)
a, b:positive
(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~0) -> (p | b~0) -> (p | (gcdn n a b)~0)
(* Lt *)
n:nat
IHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p0 : positive, (p0 | a0) -> (p0 | b0) -> (p0 | gcdn n a0 b0)
a, b:positive
LT:a < b
LE:(S (size_nat a + S (size_nat b)) <= S n)%nat
p:positive
Hp1:(p | a~1)
Hp2:(p | b~1)

(p | gcdn n (b - a) a~1)
n:nat
IHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)
a, b:positive
b < a -> (S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~1) -> (p | b~1) -> (p | gcdn n (a - b) b~1)
n:nat
IHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)
a, b:positive
(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~1) -> (p | b~0) -> (p | gcdn n a~1 b)
n:nat
IHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)
a, b:positive
(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~0) -> (p | b~1) -> (p | gcdn n a b~1)
n:nat
IHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)
a, b:positive
(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~0) -> (p | b~0) -> (p | (gcdn n a b)~0)
n:nat
a, b:positive
LT:a < b
LE:(S (size_nat a + S (size_nat b)) <= S n)%nat
p:positive
Hp1:(p | a~1)
Hp2:(p | b~1)

(size_nat (b - a) + size_nat a~1 <= n)%nat
n:nat
a, b:positive
LT:a < b
LE:(S (size_nat a + S (size_nat b)) <= S n)%nat
p:positive
Hp1:(p | a~1)
Hp2:(p | b~1)
(p | b - a)
n:nat
IHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)
a, b:positive
b < a -> (S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~1) -> (p | b~1) -> (p | gcdn n (a - b) b~1)
n:nat
IHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)
a, b:positive
(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~1) -> (p | b~0) -> (p | gcdn n a~1 b)
n:nat
IHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)
a, b:positive
(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~0) -> (p | b~1) -> (p | gcdn n a b~1)
n:nat
IHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)
a, b:positive
(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~0) -> (p | b~0) -> (p | (gcdn n a b)~0)
n:nat
a, b:positive
LT:a < b
LE:(size_nat a + S (size_nat b) <= n)%nat
p:positive
Hp1:(p | a~1)
Hp2:(p | b~1)

(size_nat (b - a) + size_nat a~1 <= n)%nat
n:nat
a, b:positive
LT:a < b
LE:(S (size_nat a + S (size_nat b)) <= S n)%nat
p:positive
Hp1:(p | a~1)
Hp2:(p | b~1)
(p | b - a)
n:nat
IHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)
a, b:positive
b < a -> (S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~1) -> (p | b~1) -> (p | gcdn n (a - b) b~1)
n:nat
IHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)
a, b:positive
(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~1) -> (p | b~0) -> (p | gcdn n a~1 b)
n:nat
IHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)
a, b:positive
(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~0) -> (p | b~1) -> (p | gcdn n a b~1)
n:nat
IHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)
a, b:positive
(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~0) -> (p | b~0) -> (p | (gcdn n a b)~0)
n:nat
a, b:positive
LT:a < b
LE:(size_nat a + S (size_nat b) <= n)%nat
p:positive
Hp1:(p | a~1)
Hp2:(p | b~1)

(size_nat (b - a) + size_nat a~1 <= size_nat a + S (size_nat b))%nat
n:nat
a, b:positive
LT:a < b
LE:(S (size_nat a + S (size_nat b)) <= S n)%nat
p:positive
Hp1:(p | a~1)
Hp2:(p | b~1)
(p | b - a)
n:nat
IHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)
a, b:positive
b < a -> (S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~1) -> (p | b~1) -> (p | gcdn n (a - b) b~1)
n:nat
IHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)
a, b:positive
(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~1) -> (p | b~0) -> (p | gcdn n a~1 b)
n:nat
IHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)
a, b:positive
(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~0) -> (p | b~1) -> (p | gcdn n a b~1)
n:nat
IHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)
a, b:positive
(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~0) -> (p | b~0) -> (p | (gcdn n a b)~0)
n:nat
a, b:positive
LT:a < b
LE:(size_nat a + S (size_nat b) <= n)%nat
p:positive
Hp1:(p | a~1)
Hp2:(p | b~1)

(size_nat a~1 + size_nat (b - a) <= S (size_nat a) + size_nat b)%nat
n:nat
a, b:positive
LT:a < b
LE:(S (size_nat a + S (size_nat b)) <= S n)%nat
p:positive
Hp1:(p | a~1)
Hp2:(p | b~1)
(p | b - a)
n:nat
IHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)
a, b:positive
b < a -> (S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~1) -> (p | b~1) -> (p | gcdn n (a - b) b~1)
n:nat
IHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)
a, b:positive
(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~1) -> (p | b~0) -> (p | gcdn n a~1 b)
n:nat
IHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)
a, b:positive
(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~0) -> (p | b~1) -> (p | gcdn n a b~1)
n:nat
IHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)
a, b:positive
(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~0) -> (p | b~0) -> (p | (gcdn n a b)~0)
n:nat
a, b:positive
LT:a < b
LE:(size_nat a + S (size_nat b) <= n)%nat
p:positive
Hp1:(p | a~1)
Hp2:(p | b~1)

(size_nat (b - a) <= size_nat b)%nat
n:nat
a, b:positive
LT:a < b
LE:(S (size_nat a + S (size_nat b)) <= S n)%nat
p:positive
Hp1:(p | a~1)
Hp2:(p | b~1)
(p | b - a)
n:nat
IHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)
a, b:positive
b < a -> (S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~1) -> (p | b~1) -> (p | gcdn n (a - b) b~1)
n:nat
IHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)
a, b:positive
(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~1) -> (p | b~0) -> (p | gcdn n a~1 b)
n:nat
IHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)
a, b:positive
(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~0) -> (p | b~1) -> (p | gcdn n a b~1)
n:nat
IHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)
a, b:positive
(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~0) -> (p | b~0) -> (p | (gcdn n a b)~0)
n:nat
a, b:positive
LT:a < b
LE:(S (size_nat a + S (size_nat b)) <= S n)%nat
p:positive
Hp1:(p | a~1)
Hp2:(p | b~1)

(p | b - a)
n:nat
IHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)
a, b:positive
b < a -> (S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~1) -> (p | b~1) -> (p | gcdn n (a - b) b~1)
n:nat
IHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)
a, b:positive
(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~1) -> (p | b~0) -> (p | gcdn n a~1 b)
n:nat
IHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)
a, b:positive
(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~0) -> (p | b~1) -> (p | gcdn n a b~1)
n:nat
IHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)
a, b:positive
(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~0) -> (p | b~0) -> (p | (gcdn n a b)~0)
n:nat
a, b:positive
LT:a < b
LE:(S (size_nat a + S (size_nat b)) <= S n)%nat
p:positive
Hp1:(p | a~1)
Hp2:(p | b~1)

(p | (b - a)~0)
n:nat
IHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)
a, b:positive
b < a -> (S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~1) -> (p | b~1) -> (p | gcdn n (a - b) b~1)
n:nat
IHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)
a, b:positive
(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~1) -> (p | b~0) -> (p | gcdn n a~1 b)
n:nat
IHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)
a, b:positive
(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~0) -> (p | b~1) -> (p | gcdn n a b~1)
n:nat
IHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)
a, b:positive
(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~0) -> (p | b~0) -> (p | (gcdn n a b)~0)
n:nat
a, b:positive
LT:a < b
LE:(S (size_nat a + S (size_nat b)) <= S n)%nat
p:positive
Hp1:(p | a~1)
Hp2:(p | b~1)

(p | (b - a)~0 + a~1)
n:nat
IHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)
a, b:positive
b < a -> (S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~1) -> (p | b~1) -> (p | gcdn n (a - b) b~1)
n:nat
IHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)
a, b:positive
(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~1) -> (p | b~0) -> (p | gcdn n a~1 b)
n:nat
IHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)
a, b:positive
(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~0) -> (p | b~1) -> (p | gcdn n a b~1)
n:nat
IHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)
a, b:positive
(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~0) -> (p | b~0) -> (p | (gcdn n a b)~0)
n:nat
IHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)
a, b:positive

b < a -> (S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~1) -> (p | b~1) -> (p | gcdn n (a - b) b~1)
n:nat
IHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)
a, b:positive
(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~1) -> (p | b~0) -> (p | gcdn n a~1 b)
n:nat
IHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)
a, b:positive
(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~0) -> (p | b~1) -> (p | gcdn n a b~1)
n:nat
IHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)
a, b:positive
(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~0) -> (p | b~0) -> (p | (gcdn n a b)~0)
(* Gt *)
n:nat
IHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p0 : positive, (p0 | a0) -> (p0 | b0) -> (p0 | gcdn n a0 b0)
a, b:positive
LT:b < a
LE:(S (size_nat a + S (size_nat b)) <= S n)%nat
p:positive
Hp1:(p | a~1)
Hp2:(p | b~1)

(p | gcdn n (a - b) b~1)
n:nat
IHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)
a, b:positive
(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~1) -> (p | b~0) -> (p | gcdn n a~1 b)
n:nat
IHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)
a, b:positive
(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~0) -> (p | b~1) -> (p | gcdn n a b~1)
n:nat
IHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)
a, b:positive
(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~0) -> (p | b~0) -> (p | (gcdn n a b)~0)
n:nat
a, b:positive
LT:b < a
LE:(S (size_nat a + S (size_nat b)) <= S n)%nat
p:positive
Hp1:(p | a~1)
Hp2:(p | b~1)

(size_nat (a - b) + size_nat b~1 <= n)%nat
n:nat
a, b:positive
LT:b < a
LE:(S (size_nat a + S (size_nat b)) <= S n)%nat
p:positive
Hp1:(p | a~1)
Hp2:(p | b~1)
(p | a - b)
n:nat
IHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)
a, b:positive
(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~1) -> (p | b~0) -> (p | gcdn n a~1 b)
n:nat
IHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)
a, b:positive
(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~0) -> (p | b~1) -> (p | gcdn n a b~1)
n:nat
IHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)
a, b:positive
(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~0) -> (p | b~0) -> (p | (gcdn n a b)~0)
n:nat
a, b:positive
LT:b < a
LE:(size_nat a + S (size_nat b) <= n)%nat
p:positive
Hp1:(p | a~1)
Hp2:(p | b~1)

(size_nat (a - b) + size_nat b~1 <= n)%nat
n:nat
a, b:positive
LT:b < a
LE:(S (size_nat a + S (size_nat b)) <= S n)%nat
p:positive
Hp1:(p | a~1)
Hp2:(p | b~1)
(p | a - b)
n:nat
IHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)
a, b:positive
(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~1) -> (p | b~0) -> (p | gcdn n a~1 b)
n:nat
IHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)
a, b:positive
(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~0) -> (p | b~1) -> (p | gcdn n a b~1)
n:nat
IHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)
a, b:positive
(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~0) -> (p | b~0) -> (p | (gcdn n a b)~0)
n:nat
a, b:positive
LT:b < a
LE:(size_nat a + S (size_nat b) <= n)%nat
p:positive
Hp1:(p | a~1)
Hp2:(p | b~1)

(size_nat (a - b) + size_nat b~1 <= size_nat a + S (size_nat b))%nat
n:nat
a, b:positive
LT:b < a
LE:(S (size_nat a + S (size_nat b)) <= S n)%nat
p:positive
Hp1:(p | a~1)
Hp2:(p | b~1)
(p | a - b)
n:nat
IHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)
a, b:positive
(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~1) -> (p | b~0) -> (p | gcdn n a~1 b)
n:nat
IHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)
a, b:positive
(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~0) -> (p | b~1) -> (p | gcdn n a b~1)
n:nat
IHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)
a, b:positive
(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~0) -> (p | b~0) -> (p | (gcdn n a b)~0)
n:nat
a, b:positive
LT:b < a
LE:(size_nat a + S (size_nat b) <= n)%nat
p:positive
Hp1:(p | a~1)
Hp2:(p | b~1)

(size_nat (a - b) <= size_nat a)%nat
n:nat
a, b:positive
LT:b < a
LE:(S (size_nat a + S (size_nat b)) <= S n)%nat
p:positive
Hp1:(p | a~1)
Hp2:(p | b~1)
(p | a - b)
n:nat
IHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)
a, b:positive
(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~1) -> (p | b~0) -> (p | gcdn n a~1 b)
n:nat
IHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)
a, b:positive
(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~0) -> (p | b~1) -> (p | gcdn n a b~1)
n:nat
IHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)
a, b:positive
(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~0) -> (p | b~0) -> (p | (gcdn n a b)~0)
n:nat
a, b:positive
LT:b < a
LE:(S (size_nat a + S (size_nat b)) <= S n)%nat
p:positive
Hp1:(p | a~1)
Hp2:(p | b~1)

(p | a - b)
n:nat
IHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)
a, b:positive
(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~1) -> (p | b~0) -> (p | gcdn n a~1 b)
n:nat
IHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)
a, b:positive
(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~0) -> (p | b~1) -> (p | gcdn n a b~1)
n:nat
IHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)
a, b:positive
(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~0) -> (p | b~0) -> (p | (gcdn n a b)~0)
n:nat
a, b:positive
LT:b < a
LE:(S (size_nat a + S (size_nat b)) <= S n)%nat
p:positive
Hp1:(p | a~1)
Hp2:(p | b~1)

(p | (a - b)~0)
n:nat
IHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)
a, b:positive
(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~1) -> (p | b~0) -> (p | gcdn n a~1 b)
n:nat
IHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)
a, b:positive
(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~0) -> (p | b~1) -> (p | gcdn n a b~1)
n:nat
IHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)
a, b:positive
(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~0) -> (p | b~0) -> (p | (gcdn n a b)~0)
n:nat
a, b:positive
LT:b < a
LE:(S (size_nat a + S (size_nat b)) <= S n)%nat
p:positive
Hp1:(p | a~1)
Hp2:(p | b~1)

(p | (a - b)~0 + b~1)
n:nat
IHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)
a, b:positive
(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~1) -> (p | b~0) -> (p | gcdn n a~1 b)
n:nat
IHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)
a, b:positive
(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~0) -> (p | b~1) -> (p | gcdn n a b~1)
n:nat
IHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)
a, b:positive
(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~0) -> (p | b~0) -> (p | (gcdn n a b)~0)
n:nat
IHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)
a, b:positive

(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~1) -> (p | b~0) -> (p | gcdn n a~1 b)
n:nat
IHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)
a, b:positive
(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~0) -> (p | b~1) -> (p | gcdn n a b~1)
n:nat
IHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)
a, b:positive
(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~0) -> (p | b~0) -> (p | (gcdn n a b)~0)
(* a~1 b~0 *)
n:nat
IHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p0 : positive, (p0 | a0) -> (p0 | b0) -> (p0 | gcdn n a0 b0)
a, b:positive
LE:(S (size_nat a + S (size_nat b)) <= S n)%nat
p:positive
Hp1:(p | a~1)
Hp2:(p | b~0)

(p | gcdn n a~1 b)
n:nat
IHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)
a, b:positive
(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~0) -> (p | b~1) -> (p | gcdn n a b~1)
n:nat
IHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)
a, b:positive
(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~0) -> (p | b~0) -> (p | (gcdn n a b)~0)
n:nat
a, b:positive
LE:(S (size_nat a + S (size_nat b)) <= S n)%nat
p:positive
Hp1:(p | a~1)
Hp2:(p | b~0)

(size_nat a~1 + size_nat b <= n)%nat
n:nat
a, b:positive
LE:(S (size_nat a + S (size_nat b)) <= S n)%nat
p:positive
Hp1:(p | a~1)
Hp2:(p | b~0)
(p | b)
n:nat
IHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)
a, b:positive
(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~0) -> (p | b~1) -> (p | gcdn n a b~1)
n:nat
IHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)
a, b:positive
(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~0) -> (p | b~0) -> (p | (gcdn n a b)~0)
n:nat
a, b:positive
LE:(size_nat a + S (size_nat b) <= n)%nat
p:positive
Hp1:(p | a~1)
Hp2:(p | b~0)

(size_nat a~1 + size_nat b <= n)%nat
n:nat
a, b:positive
LE:(S (size_nat a + S (size_nat b)) <= S n)%nat
p:positive
Hp1:(p | a~1)
Hp2:(p | b~0)
(p | b)
n:nat
IHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)
a, b:positive
(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~0) -> (p | b~1) -> (p | gcdn n a b~1)
n:nat
IHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)
a, b:positive
(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~0) -> (p | b~0) -> (p | (gcdn n a b)~0)
n:nat
a, b:positive
LE:(size_nat a + S (size_nat b) <= n)%nat
p:positive
Hp1:(p | a~1)
Hp2:(p | b~0)

(S (size_nat a + size_nat b) <= n)%nat
n:nat
a, b:positive
LE:(S (size_nat a + S (size_nat b)) <= S n)%nat
p:positive
Hp1:(p | a~1)
Hp2:(p | b~0)
(p | b)
n:nat
IHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)
a, b:positive
(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~0) -> (p | b~1) -> (p | gcdn n a b~1)
n:nat
IHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)
a, b:positive
(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~0) -> (p | b~0) -> (p | (gcdn n a b)~0)
n:nat
a, b:positive
LE:(S (size_nat a + S (size_nat b)) <= S n)%nat
p:positive
Hp1:(p | a~1)
Hp2:(p | b~0)

(p | b)
n:nat
IHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)
a, b:positive
(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~0) -> (p | b~1) -> (p | gcdn n a b~1)
n:nat
IHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)
a, b:positive
(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~0) -> (p | b~0) -> (p | (gcdn n a b)~0)
n:nat
IHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)
a, b:positive

(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~0) -> (p | b~1) -> (p | gcdn n a b~1)
n:nat
IHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)
a, b:positive
(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~0) -> (p | b~0) -> (p | (gcdn n a b)~0)
(* a~0 b~1 *)
n:nat
IHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p0 : positive, (p0 | a0) -> (p0 | b0) -> (p0 | gcdn n a0 b0)
a, b:positive
LE:(S (size_nat a + S (size_nat b)) <= S n)%nat
p:positive
Hp1:(p | a~0)
Hp2:(p | b~1)

(p | gcdn n a b~1)
n:nat
IHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)
a, b:positive
(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~0) -> (p | b~0) -> (p | (gcdn n a b)~0)
n:nat
a, b:positive
LE:(S (size_nat a + S (size_nat b)) <= S n)%nat
p:positive
Hp1:(p | a~0)
Hp2:(p | b~1)

(size_nat a + size_nat b~1 <= n)%nat
n:nat
a, b:positive
LE:(S (size_nat a + S (size_nat b)) <= S n)%nat
p:positive
Hp1:(p | a~0)
Hp2:(p | b~1)
(p | a)
n:nat
IHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)
a, b:positive
(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~0) -> (p | b~0) -> (p | (gcdn n a b)~0)
n:nat
a, b:positive
LE:(S (size_nat a + S (size_nat b)) <= S n)%nat
p:positive
Hp1:(p | a~0)
Hp2:(p | b~1)

(size_nat a + S (size_nat b) <= n)%nat
n:nat
a, b:positive
LE:(S (size_nat a + S (size_nat b)) <= S n)%nat
p:positive
Hp1:(p | a~0)
Hp2:(p | b~1)
(p | a)
n:nat
IHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)
a, b:positive
(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~0) -> (p | b~0) -> (p | (gcdn n a b)~0)
n:nat
a, b:positive
LE:(S (size_nat a + S (size_nat b)) <= S n)%nat
p:positive
Hp1:(p | a~0)
Hp2:(p | b~1)

(p | a)
n:nat
IHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)
a, b:positive
(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~0) -> (p | b~0) -> (p | (gcdn n a b)~0)
n:nat
IHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)
a, b:positive

(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~0) -> (p | b~0) -> (p | (gcdn n a b)~0)
(* a~0 b~0 *)
n:nat
IHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p0 : positive, (p0 | a0) -> (p0 | b0) -> (p0 | gcdn n a0 b0)
a, b:positive
LE:(S (size_nat a + S (size_nat b)) <= S n)%nat
p:positive
Hp1:(p | a~0)
Hp2:(p | b~0)

(p | (gcdn n a b)~0)
n:nat
IHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p0 : positive, (p0 | a0) -> (p0 | b0) -> (p0 | gcdn n a0 b0)
a, b:positive
LE:(S (size_nat a + S (size_nat b)) <= S n)%nat
p:positive
Hp1:(p~1 | a~0)
Hp2:(p~1 | b~0)

(p~1 | (gcdn n a b)~0)
n:nat
IHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p0 : positive, (p0 | a0) -> (p0 | b0) -> (p0 | gcdn n a0 b0)
a, b:positive
LE:(S (size_nat a + S (size_nat b)) <= S n)%nat
p:positive
Hp1:(p~0 | a~0)
Hp2:(p~0 | b~0)
(p~0 | (gcdn n a b)~0)
n:nat
IHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)
a, b:positive
LE:(S (size_nat a + S (size_nat b)) <= S n)%nat
Hp1:(1 | a~0)
Hp2:(1 | b~0)
(1 | (gcdn n a b)~0)
n:nat
IHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p0 : positive, (p0 | a0) -> (p0 | b0) -> (p0 | gcdn n a0 b0)
a, b:positive
LE:(S (size_nat a + S (size_nat b)) <= S n)%nat
p:positive
Hp1:(p~1 | a~0)
Hp2:(p~1 | b~0)

(p~1 | 2 * gcdn n a b)
n:nat
IHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p0 : positive, (p0 | a0) -> (p0 | b0) -> (p0 | gcdn n a0 b0)
a, b:positive
LE:(S (size_nat a + S (size_nat b)) <= S n)%nat
p:positive
Hp1:(p~0 | a~0)
Hp2:(p~0 | b~0)
(p~0 | (gcdn n a b)~0)
n:nat
IHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)
a, b:positive
LE:(S (size_nat a + S (size_nat b)) <= S n)%nat
Hp1:(1 | a~0)
Hp2:(1 | b~0)
(1 | (gcdn n a b)~0)
n:nat
IHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p0 : positive, (p0 | a0) -> (p0 | b0) -> (p0 | gcdn n a0 b0)
a, b:positive
LE:(S (size_nat a + S (size_nat b)) <= S n)%nat
p:positive
Hp1:(p~1 | a~0)
Hp2:(p~1 | b~0)

(p~1 | gcdn n a b)
n:nat
IHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p0 : positive, (p0 | a0) -> (p0 | b0) -> (p0 | gcdn n a0 b0)
a, b:positive
LE:(S (size_nat a + S (size_nat b)) <= S n)%nat
p:positive
Hp1:(p~0 | a~0)
Hp2:(p~0 | b~0)
(p~0 | (gcdn n a b)~0)
n:nat
IHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)
a, b:positive
LE:(S (size_nat a + S (size_nat b)) <= S n)%nat
Hp1:(1 | a~0)
Hp2:(1 | b~0)
(1 | (gcdn n a b)~0)
n:nat
a, b:positive
LE:(S (size_nat a + S (size_nat b)) <= S n)%nat
p:positive
Hp1:(p~1 | a~0)
Hp2:(p~1 | b~0)

(size_nat a + size_nat b <= n)%nat
n:nat
a, b:positive
LE:(S (size_nat a + S (size_nat b)) <= S n)%nat
p:positive
Hp1:(p~1 | a~0)
Hp2:(p~1 | b~0)
(p~1 | a)
n:nat
a, b:positive
LE:(S (size_nat a + S (size_nat b)) <= S n)%nat
p:positive
Hp1:(p~1 | a~0)
Hp2:(p~1 | b~0)
(p~1 | b)
n:nat
IHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p0 : positive, (p0 | a0) -> (p0 | b0) -> (p0 | gcdn n a0 b0)
a, b:positive
LE:(S (size_nat a + S (size_nat b)) <= S n)%nat
p:positive
Hp1:(p~0 | a~0)
Hp2:(p~0 | b~0)
(p~0 | (gcdn n a b)~0)
n:nat
IHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)
a, b:positive
LE:(S (size_nat a + S (size_nat b)) <= S n)%nat
Hp1:(1 | a~0)
Hp2:(1 | b~0)
(1 | (gcdn n a b)~0)
n:nat
a, b:positive
LE:(size_nat a + S (size_nat b) <= n)%nat
p:positive
Hp1:(p~1 | a~0)
Hp2:(p~1 | b~0)

(size_nat a + size_nat b <= n)%nat
n:nat
a, b:positive
LE:(S (size_nat a + S (size_nat b)) <= S n)%nat
p:positive
Hp1:(p~1 | a~0)
Hp2:(p~1 | b~0)
(p~1 | a)
n:nat
a, b:positive
LE:(S (size_nat a + S (size_nat b)) <= S n)%nat
p:positive
Hp1:(p~1 | a~0)
Hp2:(p~1 | b~0)
(p~1 | b)
n:nat
IHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p0 : positive, (p0 | a0) -> (p0 | b0) -> (p0 | gcdn n a0 b0)
a, b:positive
LE:(S (size_nat a + S (size_nat b)) <= S n)%nat
p:positive
Hp1:(p~0 | a~0)
Hp2:(p~0 | b~0)
(p~0 | (gcdn n a b)~0)
n:nat
IHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)
a, b:positive
LE:(S (size_nat a + S (size_nat b)) <= S n)%nat
Hp1:(1 | a~0)
Hp2:(1 | b~0)
(1 | (gcdn n a b)~0)
n:nat
a, b:positive
LE:(size_nat a + S (size_nat b) <= n)%nat
p:positive
Hp1:(p~1 | a~0)
Hp2:(p~1 | b~0)

(S (size_nat a + size_nat b) <= n)%nat
n:nat
a, b:positive
LE:(S (size_nat a + S (size_nat b)) <= S n)%nat
p:positive
Hp1:(p~1 | a~0)
Hp2:(p~1 | b~0)
(p~1 | a)
n:nat
a, b:positive
LE:(S (size_nat a + S (size_nat b)) <= S n)%nat
p:positive
Hp1:(p~1 | a~0)
Hp2:(p~1 | b~0)
(p~1 | b)
n:nat
IHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p0 : positive, (p0 | a0) -> (p0 | b0) -> (p0 | gcdn n a0 b0)
a, b:positive
LE:(S (size_nat a + S (size_nat b)) <= S n)%nat
p:positive
Hp1:(p~0 | a~0)
Hp2:(p~0 | b~0)
(p~0 | (gcdn n a b)~0)
n:nat
IHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)
a, b:positive
LE:(S (size_nat a + S (size_nat b)) <= S n)%nat
Hp1:(1 | a~0)
Hp2:(1 | b~0)
(1 | (gcdn n a b)~0)
n:nat
a, b:positive
LE:(S (size_nat a + S (size_nat b)) <= S n)%nat
p:positive
Hp1:(p~1 | a~0)
Hp2:(p~1 | b~0)

(p~1 | a)
n:nat
a, b:positive
LE:(S (size_nat a + S (size_nat b)) <= S n)%nat
p:positive
Hp1:(p~1 | a~0)
Hp2:(p~1 | b~0)
(p~1 | b)
n:nat
IHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p0 : positive, (p0 | a0) -> (p0 | b0) -> (p0 | gcdn n a0 b0)
a, b:positive
LE:(S (size_nat a + S (size_nat b)) <= S n)%nat
p:positive
Hp1:(p~0 | a~0)
Hp2:(p~0 | b~0)
(p~0 | (gcdn n a b)~0)
n:nat
IHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)
a, b:positive
LE:(S (size_nat a + S (size_nat b)) <= S n)%nat
Hp1:(1 | a~0)
Hp2:(1 | b~0)
(1 | (gcdn n a b)~0)
n:nat
a, b:positive
LE:(S (size_nat a + S (size_nat b)) <= S n)%nat
p:positive
Hp1:(p~1 | a~0)
Hp2:(p~1 | b~0)

(p~1 | p~1)
n:nat
a, b:positive
LE:(S (size_nat a + S (size_nat b)) <= S n)%nat
p:positive
Hp1:(p~1 | a~0)
Hp2:(p~1 | b~0)
(p~1 | b)
n:nat
IHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p0 : positive, (p0 | a0) -> (p0 | b0) -> (p0 | gcdn n a0 b0)
a, b:positive
LE:(S (size_nat a + S (size_nat b)) <= S n)%nat
p:positive
Hp1:(p~0 | a~0)
Hp2:(p~0 | b~0)
(p~0 | (gcdn n a b)~0)
n:nat
IHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)
a, b:positive
LE:(S (size_nat a + S (size_nat b)) <= S n)%nat
Hp1:(1 | a~0)
Hp2:(1 | b~0)
(1 | (gcdn n a b)~0)
n:nat
a, b:positive
LE:(S (size_nat a + S (size_nat b)) <= S n)%nat
p:positive
Hp1:(p~1 | a~0)
Hp2:(p~1 | b~0)

(p~1 | b)
n:nat
IHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p0 : positive, (p0 | a0) -> (p0 | b0) -> (p0 | gcdn n a0 b0)
a, b:positive
LE:(S (size_nat a + S (size_nat b)) <= S n)%nat
p:positive
Hp1:(p~0 | a~0)
Hp2:(p~0 | b~0)
(p~0 | (gcdn n a b)~0)
n:nat
IHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)
a, b:positive
LE:(S (size_nat a + S (size_nat b)) <= S n)%nat
Hp1:(1 | a~0)
Hp2:(1 | b~0)
(1 | (gcdn n a b)~0)
n:nat
a, b:positive
LE:(S (size_nat a + S (size_nat b)) <= S n)%nat
p:positive
Hp1:(p~1 | a~0)
Hp2:(p~1 | b~0)

(p~1 | p~1)
n:nat
IHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p0 : positive, (p0 | a0) -> (p0 | b0) -> (p0 | gcdn n a0 b0)
a, b:positive
LE:(S (size_nat a + S (size_nat b)) <= S n)%nat
p:positive
Hp1:(p~0 | a~0)
Hp2:(p~0 | b~0)
(p~0 | (gcdn n a b)~0)
n:nat
IHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)
a, b:positive
LE:(S (size_nat a + S (size_nat b)) <= S n)%nat
Hp1:(1 | a~0)
Hp2:(1 | b~0)
(1 | (gcdn n a b)~0)
n:nat
IHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p0 : positive, (p0 | a0) -> (p0 | b0) -> (p0 | gcdn n a0 b0)
a, b:positive
LE:(S (size_nat a + S (size_nat b)) <= S n)%nat
p:positive
Hp1:(p~0 | a~0)
Hp2:(p~0 | b~0)

(p~0 | (gcdn n a b)~0)
n:nat
IHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)
a, b:positive
LE:(S (size_nat a + S (size_nat b)) <= S n)%nat
Hp1:(1 | a~0)
Hp2:(1 | b~0)
(1 | (gcdn n a b)~0)
n:nat
IHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p0 : positive, (p0 | a0) -> (p0 | b0) -> (p0 | gcdn n a0 b0)
a, b:positive
LE:(S (size_nat a + S (size_nat b)) <= S n)%nat
p:positive
Hp1:(p~0 | a~0)
Hp2:(p~0 | b~0)

(p | gcdn n a b)
n:nat
IHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)
a, b:positive
LE:(S (size_nat a + S (size_nat b)) <= S n)%nat
Hp1:(1 | a~0)
Hp2:(1 | b~0)
(1 | (gcdn n a b)~0)
n:nat
a, b:positive
LE:(S (size_nat a + S (size_nat b)) <= S n)%nat
p:positive
Hp1:(p~0 | a~0)
Hp2:(p~0 | b~0)

(size_nat a + size_nat b <= n)%nat
n:nat
a, b:positive
LE:(S (size_nat a + S (size_nat b)) <= S n)%nat
p:positive
Hp1:(p~0 | a~0)
Hp2:(p~0 | b~0)
(p | a)
n:nat
a, b:positive
LE:(S (size_nat a + S (size_nat b)) <= S n)%nat
p:positive
Hp1:(p~0 | a~0)
Hp2:(p~0 | b~0)
(p | b)
n:nat
IHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)
a, b:positive
LE:(S (size_nat a + S (size_nat b)) <= S n)%nat
Hp1:(1 | a~0)
Hp2:(1 | b~0)
(1 | (gcdn n a b)~0)
n:nat
a, b:positive
LE:(size_nat a + S (size_nat b) <= n)%nat
p:positive
Hp1:(p~0 | a~0)
Hp2:(p~0 | b~0)

(size_nat a + size_nat b <= n)%nat
n:nat
a, b:positive
LE:(S (size_nat a + S (size_nat b)) <= S n)%nat
p:positive
Hp1:(p~0 | a~0)
Hp2:(p~0 | b~0)
(p | a)
n:nat
a, b:positive
LE:(S (size_nat a + S (size_nat b)) <= S n)%nat
p:positive
Hp1:(p~0 | a~0)
Hp2:(p~0 | b~0)
(p | b)
n:nat
IHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)
a, b:positive
LE:(S (size_nat a + S (size_nat b)) <= S n)%nat
Hp1:(1 | a~0)
Hp2:(1 | b~0)
(1 | (gcdn n a b)~0)
n:nat
a, b:positive
LE:(size_nat a + S (size_nat b) <= n)%nat
p:positive
Hp1:(p~0 | a~0)
Hp2:(p~0 | b~0)

(S (size_nat a + size_nat b) <= n)%nat
n:nat
a, b:positive
LE:(S (size_nat a + S (size_nat b)) <= S n)%nat
p:positive
Hp1:(p~0 | a~0)
Hp2:(p~0 | b~0)
(p | a)
n:nat
a, b:positive
LE:(S (size_nat a + S (size_nat b)) <= S n)%nat
p:positive
Hp1:(p~0 | a~0)
Hp2:(p~0 | b~0)
(p | b)
n:nat
IHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)
a, b:positive
LE:(S (size_nat a + S (size_nat b)) <= S n)%nat
Hp1:(1 | a~0)
Hp2:(1 | b~0)
(1 | (gcdn n a b)~0)
n:nat
a, b:positive
LE:(S (size_nat a + S (size_nat b)) <= S n)%nat
p:positive
Hp1:(p~0 | a~0)
Hp2:(p~0 | b~0)

(p | a)
n:nat
a, b:positive
LE:(S (size_nat a + S (size_nat b)) <= S n)%nat
p:positive
Hp1:(p~0 | a~0)
Hp2:(p~0 | b~0)
(p | b)
n:nat
IHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)
a, b:positive
LE:(S (size_nat a + S (size_nat b)) <= S n)%nat
Hp1:(1 | a~0)
Hp2:(1 | b~0)
(1 | (gcdn n a b)~0)
n:nat
a, b:positive
LE:(S (size_nat a + S (size_nat b)) <= S n)%nat
p:positive
Hp1:(p~0 | a~0)
Hp2:(p~0 | b~0)

(p | b)
n:nat
IHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)
a, b:positive
LE:(S (size_nat a + S (size_nat b)) <= S n)%nat
Hp1:(1 | a~0)
Hp2:(1 | b~0)
(1 | (gcdn n a b)~0)
n:nat
IHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)
a, b:positive
LE:(S (size_nat a + S (size_nat b)) <= S n)%nat
Hp1:(1 | a~0)
Hp2:(1 | b~0)

(1 | (gcdn n a b)~0)
n:nat
IHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)
a, b:positive
LE:(S (size_nat a + S (size_nat b)) <= S n)%nat
Hp1:(1 | a~0)
Hp2:(1 | b~0)

(gcdn n a b)~0 = (gcdn n a b)~0 * 1
now rewrite mul_1_r. Qed.

forall a b p : positive, (p | a) -> (p | b) -> (p | gcd a b)

forall a b p : positive, (p | a) -> (p | b) -> (p | gcd a b)
a, b, p:positive
H:(p | a)
H0:(p | b)

(p | gcd a b)
apply gcdn_greatest; auto. Qed.
As a consequence, the rests after division by gcd are relatively prime

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

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

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

(forall p : positive, (p | a) -> (p | b) -> (p | gcd a b)) -> (let '(g, (aa, bb)) := ggcd a b in a = g * aa /\ b = g * bb) -> let (aa, bb) := snd (ggcd a b) in forall p : positive, (p | aa) -> (p | bb) -> p = 1
a, b:positive

(forall p : positive, (p | a) -> (p | b) -> (p | fst (ggcd a b))) -> (let '(g, (aa, bb)) := ggcd a b in a = g * aa /\ b = g * bb) -> let (aa, bb) := snd (ggcd a b) in forall p : positive, (p | aa) -> (p | bb) -> p = 1
a, b, g, aa, bb:positive

(forall p : positive, (p | a) -> (p | b) -> (p | g)) -> a = g * aa /\ b = g * bb -> forall p : positive, (p | aa) -> (p | bb) -> p = 1
g, aa, bb:positive
H:forall p0 : positive, (p0 | g * aa) -> (p0 | g * bb) -> (p0 | g)
p:positive
Hp1:(p | aa)
Hp2:(p | bb)

p = 1
g, aa, bb:positive
H:forall p0 : positive, (p0 | g * aa) -> (p0 | g * bb) -> (p0 | g)
p:positive
Hp1:(p | aa)
Hp2:(p | bb)

(g * p | g)
g, aa, bb:positive
H:forall p0 : positive, (p0 | g * aa) -> (p0 | g * bb) -> (p0 | g)
p:positive
Hp1:(p | aa)
Hp2:(p | bb)
H':(g * p | g)
p = 1
g, aa, bb:positive
H:forall p0 : positive, (p0 | g * aa) -> (p0 | g * bb) -> (p0 | g)
p:positive
Hp1:(p | aa)
Hp2:(p | bb)

(g * p | g * aa)
g, aa, bb:positive
H:forall p0 : positive, (p0 | g * aa) -> (p0 | g * bb) -> (p0 | g)
p:positive
Hp1:(p | aa)
Hp2:(p | bb)
(g * p | g * bb)
g, aa, bb:positive
H:forall p0 : positive, (p0 | g * aa) -> (p0 | g * bb) -> (p0 | g)
p:positive
Hp1:(p | aa)
Hp2:(p | bb)
H':(g * p | g)
p = 1
g, aa, bb:positive
H:forall p0 : positive, (p0 | g * aa) -> (p0 | g * bb) -> (p0 | g)
p, r:positive
Hr:aa = r * p
Hp2:(p | bb)

(g * p | g * aa)
g, aa, bb:positive
H:forall p0 : positive, (p0 | g * aa) -> (p0 | g * bb) -> (p0 | g)
p:positive
Hp1:(p | aa)
Hp2:(p | bb)
(g * p | g * bb)
g, aa, bb:positive
H:forall p0 : positive, (p0 | g * aa) -> (p0 | g * bb) -> (p0 | g)
p:positive
Hp1:(p | aa)
Hp2:(p | bb)
H':(g * p | g)
p = 1
g, aa, bb:positive
H:forall p0 : positive, (p0 | g * aa) -> (p0 | g * bb) -> (p0 | g)
p, r:positive
Hr:aa = r * p
Hp2:(p | bb)

g * aa = r * (g * p)
g, aa, bb:positive
H:forall p0 : positive, (p0 | g * aa) -> (p0 | g * bb) -> (p0 | g)
p:positive
Hp1:(p | aa)
Hp2:(p | bb)
(g * p | g * bb)
g, aa, bb:positive
H:forall p0 : positive, (p0 | g * aa) -> (p0 | g * bb) -> (p0 | g)
p:positive
Hp1:(p | aa)
Hp2:(p | bb)
H':(g * p | g)
p = 1
g, aa, bb:positive
H:forall p0 : positive, (p0 | g * aa) -> (p0 | g * bb) -> (p0 | g)
p:positive
Hp1:(p | aa)
Hp2:(p | bb)

(g * p | g * bb)
g, aa, bb:positive
H:forall p0 : positive, (p0 | g * aa) -> (p0 | g * bb) -> (p0 | g)
p:positive
Hp1:(p | aa)
Hp2:(p | bb)
H':(g * p | g)
p = 1
g, aa, bb:positive
H:forall p0 : positive, (p0 | g * aa) -> (p0 | g * bb) -> (p0 | g)
p:positive
Hp1:(p | aa)
r:positive
Hr:bb = r * p

(g * p | g * bb)
g, aa, bb:positive
H:forall p0 : positive, (p0 | g * aa) -> (p0 | g * bb) -> (p0 | g)
p:positive
Hp1:(p | aa)
Hp2:(p | bb)
H':(g * p | g)
p = 1
g, aa, bb:positive
H:forall p0 : positive, (p0 | g * aa) -> (p0 | g * bb) -> (p0 | g)
p:positive
Hp1:(p | aa)
r:positive
Hr:bb = r * p

g * bb = r * (g * p)
g, aa, bb:positive
H:forall p0 : positive, (p0 | g * aa) -> (p0 | g * bb) -> (p0 | g)
p:positive
Hp1:(p | aa)
Hp2:(p | bb)
H':(g * p | g)
p = 1
g, aa, bb:positive
H:forall p0 : positive, (p0 | g * aa) -> (p0 | g * bb) -> (p0 | g)
p:positive
Hp1:(p | aa)
Hp2:(p | bb)
H':(g * p | g)

p = 1
g, aa, bb:positive
H:forall p0 : positive, (p0 | g * aa) -> (p0 | g * bb) -> (p0 | g)
p:positive
Hp1:(p | aa)
Hp2:(p | bb)
q:positive
H':g = q * (g * p)

p = 1
g, aa, bb:positive
H:forall p0 : positive, (p0 | g * aa) -> (p0 | g * bb) -> (p0 | g)
p:positive
Hp1:(p | aa)
Hp2:(p | bb)
q:positive
H':g = q * p * g

p = 1
g, aa, bb:positive
H:forall p0 : positive, (p0 | g * aa) -> (p0 | g * bb) -> (p0 | g)
p:positive
Hp1:(p | aa)
Hp2:(p | bb)
q:positive
H':g = q * p * g

q * p = 1
now apply mul_reg_r with g. Qed. End Pos. Bind Scope positive_scope with Pos.t positive.
Exportation of notations
Numeral Notation positive Pos.of_int Pos.to_uint : positive_scope.

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.
Compatibility notations
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 Pplus := Pos.add (only parsing).
Notation Pplus_carry := Pos.add_carry (only parsing).
Notation Pmult_nat := (Pos.iter_op plus) (only parsing).
Notation nat_of_P := Pos.to_nat (only parsing).
Notation P_of_succ_nat := Pos.of_succ_nat (only parsing).
Notation Pdouble_minus_one := Pos.pred_double (only parsing).
Notation positive_mask := Pos.mask (only parsing).
Notation positive_mask_rect := Pos.mask_rect (only parsing).
Notation positive_mask_ind := Pos.mask_ind (only parsing).
Notation positive_mask_rec := Pos.mask_rec (only parsing).
Notation Pdouble_plus_one_mask := Pos.succ_double_mask (only parsing).
Notation Pdouble_minus_two := Pos.double_pred_mask (only parsing).
Notation Pminus_mask := Pos.sub_mask (only parsing).
Notation Pminus_mask_carry := Pos.sub_mask_carry (only parsing).
Notation Pminus := Pos.sub (only parsing).
Notation Pmult := Pos.mul (only parsing).
Notation iter_pos := @Pos.iter (only parsing).
Notation Psize := Pos.size_nat (only parsing).
Notation Psize_pos := Pos.size (only parsing).
Notation Pcompare x y m := (Pos.compare_cont m x y) (only parsing).
Notation positive_eq_dec := Pos.eq_dec (only parsing).
Notation xI_succ_xO := Pos.xI_succ_xO (only parsing).
Notation Psucc_o_double_minus_one_eq_xO :=
 Pos.succ_pred_double (only parsing).
Notation Pdouble_minus_one_o_succ_eq_xI :=
 Pos.pred_double_succ (only parsing).
Notation xO_succ_permute := Pos.double_succ (only parsing).
Notation double_moins_un_xO_discr :=
 Pos.pred_double_xO_discr (only parsing).
Notation Psucc_not_one := Pos.succ_not_1 (only parsing).
Notation Psucc_pred := Pos.succ_pred_or (only parsing).
Notation Pplus_carry_spec := Pos.add_carry_spec (only parsing).
Notation Pplus_comm := Pos.add_comm (only parsing).
Notation Pplus_succ_permute_r := Pos.add_succ_r (only parsing).
Notation Pplus_succ_permute_l := Pos.add_succ_l (only parsing).
Notation Pplus_no_neutral := Pos.add_no_neutral (only parsing).
Notation Pplus_carry_plus := Pos.add_carry_add (only parsing).
Notation Pplus_reg_r := Pos.add_reg_r (only parsing).
Notation Pplus_reg_l := Pos.add_reg_l (only parsing).
Notation Pplus_carry_reg_r := Pos.add_carry_reg_r (only parsing).
Notation Pplus_carry_reg_l := Pos.add_carry_reg_l (only parsing).
Notation Pplus_assoc := Pos.add_assoc (only parsing).
Notation Pplus_xO := Pos.add_xO (only parsing).
Notation Pplus_xI_double_minus_one := Pos.add_xI_pred_double (only parsing).
Notation Pplus_xO_double_minus_one := Pos.add_xO_pred_double (only parsing).
Notation Pplus_diag := Pos.add_diag (only parsing).
Notation PeanoView := Pos.PeanoView (only parsing).
Notation PeanoOne := Pos.PeanoOne (only parsing).
Notation PeanoSucc := Pos.PeanoSucc (only parsing).
Notation PeanoView_rect := Pos.PeanoView_rect (only parsing).
Notation PeanoView_ind := Pos.PeanoView_ind (only parsing).
Notation PeanoView_rec := Pos.PeanoView_rec (only parsing).
Notation peanoView_xO := Pos.peanoView_xO (only parsing).
Notation peanoView_xI := Pos.peanoView_xI (only parsing).
Notation peanoView := Pos.peanoView (only parsing).
Notation PeanoView_iter := Pos.PeanoView_iter (only parsing).
Notation eq_dep_eq_positive := Pos.eq_dep_eq_positive (only parsing).
Notation PeanoViewUnique := Pos.PeanoViewUnique (only parsing).
Notation Prect := Pos.peano_rect (only parsing).
Notation Prect_succ := Pos.peano_rect_succ (only parsing).
Notation Prect_base := Pos.peano_rect_base (only parsing).
Notation Prec := Pos.peano_rec (only parsing).
Notation Pind := Pos.peano_ind (only parsing).
Notation Pcase := Pos.peano_case (only parsing).
Notation Pmult_1_r := Pos.mul_1_r (only parsing).
Notation Pmult_Sn_m := Pos.mul_succ_l (only parsing).
Notation Pmult_xO_permute_r := Pos.mul_xO_r (only parsing).
Notation Pmult_xI_permute_r := Pos.mul_xI_r (only parsing).
Notation Pmult_comm := Pos.mul_comm (only parsing).
Notation Pmult_plus_distr_l := Pos.mul_add_distr_l (only parsing).
Notation Pmult_plus_distr_r := Pos.mul_add_distr_r (only parsing).
Notation Pmult_assoc := Pos.mul_assoc (only parsing).
Notation Pmult_xI_mult_xO_discr := Pos.mul_xI_mul_xO_discr (only parsing).
Notation Pmult_xO_discr := Pos.mul_xO_discr (only parsing).
Notation Pmult_reg_r := Pos.mul_reg_r (only parsing).
Notation Pmult_reg_l := Pos.mul_reg_l (only parsing).
Notation Pmult_1_inversion_l := Pos.mul_eq_1_l (only parsing).
Notation iter_pos_swap_gen := Pos.iter_swap_gen (only parsing).
Notation iter_pos_swap := Pos.iter_swap (only parsing).
Notation iter_pos_succ := Pos.iter_succ (only parsing).
Notation iter_pos_plus := Pos.iter_add (only parsing).
Notation iter_pos_invariant := Pos.iter_invariant (only parsing).
Notation Pcompare_refl_id := Pos.compare_cont_refl (only parsing).
Notation Pcompare_eq_iff := Pos.compare_eq_iff (only parsing).
Notation Pcompare_Gt_Lt := Pos.compare_cont_Gt_Lt (only parsing).
Notation Pcompare_eq_Lt := Pos.compare_lt_iff (only parsing).
Notation Pcompare_Lt_Gt := Pos.compare_cont_Lt_Gt (only parsing).

Notation Pcompare_antisym := Pos.compare_cont_antisym (only parsing).
Notation ZC1 := Pos.gt_lt (only parsing).
Notation ZC2 := Pos.lt_gt (only parsing).
Notation Pcompare_p_Sp := Pos.lt_succ_diag_r (only parsing).
Notation Pcompare_1 := Pos.nlt_1_r (only parsing).
Notation Plt_1 := Pos.nlt_1_r (only parsing).
Notation Pplus_compare_mono_l := Pos.add_compare_mono_l (only parsing).
Notation Pplus_compare_mono_r := Pos.add_compare_mono_r (only parsing).
Notation Pplus_lt_mono_l := Pos.add_lt_mono_l (only parsing).
Notation Pplus_lt_mono_r := Pos.add_lt_mono_r (only parsing).
Notation Pplus_lt_mono := Pos.add_lt_mono (only parsing).
Notation Pplus_le_mono_l := Pos.add_le_mono_l (only parsing).
Notation Pplus_le_mono_r := Pos.add_le_mono_r (only parsing).
Notation Pplus_le_mono := Pos.add_le_mono (only parsing).
Notation Pmult_compare_mono_l := Pos.mul_compare_mono_l (only parsing).
Notation Pmult_compare_mono_r := Pos.mul_compare_mono_r (only parsing).
Notation Pmult_lt_mono_l := Pos.mul_lt_mono_l (only parsing).
Notation Pmult_lt_mono_r := Pos.mul_lt_mono_r (only parsing).
Notation Pmult_lt_mono := Pos.mul_lt_mono (only parsing).
Notation Pmult_le_mono_l := Pos.mul_le_mono_l (only parsing).
Notation Pmult_le_mono_r := Pos.mul_le_mono_r (only parsing).
Notation Pmult_le_mono := Pos.mul_le_mono (only parsing).
Notation Plt_plus_r := Pos.lt_add_r (only parsing).
Notation Plt_not_plus_l := Pos.lt_not_add_l (only parsing).
Notation Pminus_mask_succ_r := Pos.sub_mask_succ_r (only parsing).
Notation Pminus_mask_carry_spec := Pos.sub_mask_carry_spec (only parsing).
Notation Pminus_succ_r := Pos.sub_succ_r (only parsing).
Notation Pminus_mask_diag := Pos.sub_mask_diag (only parsing).

Notation Pplus_minus_eq := Pos.add_sub (only parsing).
Notation Pmult_minus_distr_l := Pos.mul_sub_distr_l (only parsing).
Notation Pminus_lt_mono_l := Pos.sub_lt_mono_l (only parsing).
Notation Pminus_compare_mono_l := Pos.sub_compare_mono_l (only parsing).
Notation Pminus_compare_mono_r := Pos.sub_compare_mono_r (only parsing).
Notation Pminus_lt_mono_r := Pos.sub_lt_mono_r (only parsing).
Notation Pminus_decr := Pos.sub_decr (only parsing).
Notation Pminus_xI_xI := Pos.sub_xI_xI (only parsing).
Notation Pplus_minus_assoc := Pos.add_sub_assoc (only parsing).
Notation Pminus_plus_distr := Pos.sub_add_distr (only parsing).
Notation Pminus_minus_distr := Pos.sub_sub_distr (only parsing).
Notation Pminus_mask_Lt := Pos.sub_mask_neg (only parsing).
Notation Pminus_Lt := Pos.sub_lt (only parsing).
Notation Pminus_Eq := Pos.sub_diag (only parsing).
Notation Psize_monotone := Pos.size_nat_monotone (only parsing).
Notation Psize_pos_gt := Pos.size_gt (only parsing).
Notation Psize_pos_le := Pos.size_le (only parsing).
More complex compatibility facts, expressed as lemmas (to preserve scopes for instance)
x, y:BinNums.positive

(x =? y) = true -> x = y
x, y:BinNums.positive

(x =? y) = true -> x = y
apply Pos.eqb_eq. Qed.
p, q:BinNums.positive

(p ?= q) = Gt <-> p > q
p, q:BinNums.positive

(p ?= q) = Gt <-> p > q
reflexivity. Qed.
p:BinNums.positive

Pos.succ p = p + 1
Proof (eq_sym (Pos.add_1_r p)).
p:BinNums.positive

Pos.succ p = 1 + p
Proof (eq_sym (Pos.add_1_l p)).
p:BinNums.positive

Pos.compare_cont Eq p p = Eq
Proof (Pos.compare_cont_refl p Eq).

forall p q : BinNums.positive, Pos.compare_cont Eq p q = Eq -> p = q
Proof Pos.compare_eq.
p, q:BinNums.positive

Pos.compare_cont Eq p q = CompOpp (Pos.compare_cont Eq q p)
Proof (Pos.compare_antisym q p).
p:BinNums.positive

Pos.pred p = p - 1
Proof (eq_sym (Pos.sub_1_r p)).
p, q:BinNums.positive

p > q -> exists h : BinNums.positive, Pos.sub_mask p q = Pos.IsPos h /\ q + h = p /\ (h = 1 \/ Pos.sub_mask_carry p q = Pos.IsPos (Pos.pred h))
p, q:BinNums.positive

p > q -> exists h : BinNums.positive, Pos.sub_mask p q = Pos.IsPos h /\ q + h = p /\ (h = 1 \/ Pos.sub_mask_carry p q = Pos.IsPos (Pos.pred h))
p, q:BinNums.positive
H:p > q

exists h : BinNums.positive, Pos.sub_mask p q = Pos.IsPos h /\ q + h = p /\ (h = 1 \/ Pos.sub_mask_carry p q = Pos.IsPos (Pos.pred h))
p, q:BinNums.positive
H:q < p

exists h : BinNums.positive, Pos.sub_mask p q = Pos.IsPos h /\ q + h = p /\ (h = 1 \/ Pos.sub_mask_carry p q = Pos.IsPos (Pos.pred h))
p, q:BinNums.positive
H:q < p
r:BinNums.positive
U:Pos.sub_mask p q = Pos.IsPos r

exists h : BinNums.positive, Pos.sub_mask p q = Pos.IsPos h /\ q + h = p /\ (h = 1 \/ Pos.sub_mask_carry p q = Pos.IsPos (Pos.pred h))
p, q:BinNums.positive
H:q < p
r:BinNums.positive
U:Pos.sub_mask p q = Pos.IsPos r

Pos.sub_mask p q = Pos.IsPos r /\ q + r = p /\ (r = 1 \/ Pos.sub_mask_carry p q = Pos.IsPos (Pos.pred r))
p, q:BinNums.positive
H:q < p
r:BinNums.positive
U:Pos.sub_mask p q = Pos.IsPos r

q + r = p
p, q:BinNums.positive
H:q < p
r:BinNums.positive
U:Pos.sub_mask p q = Pos.IsPos r
r = 1 \/ Pos.sub_mask_carry p q = Pos.IsPos (Pos.pred r)
p, q:BinNums.positive
H:q < p
r:BinNums.positive
U:Pos.sub_mask p q = Pos.IsPos r

r = 1 \/ Pos.sub_mask_carry p q = Pos.IsPos (Pos.pred r)
p, q:BinNums.positive
H:q < p
r:BinNums.positive
U:Pos.sub_mask p q = Pos.IsPos r
NE:r <> 1

Pos.sub_mask_carry p q = Pos.IsPos (Pos.pred r)
p, q:BinNums.positive
H:q < p
r:BinNums.positive
U:Pos.sub_mask p q = Pos.IsPos r
NE:r <> 1

Pos.pred_mask (Pos.IsPos r) = Pos.IsPos (Pos.pred r)
p, q:BinNums.positive
H:q < p
U:Pos.sub_mask p q = Pos.IsPos 1
NE:1 <> 1

Pos.pred_mask (Pos.IsPos 1) = Pos.IsPos (Pos.pred 1)
now elim NE. Qed.

forall p q : BinNums.positive, p > q -> q + (p - q) = p

forall p q : BinNums.positive, p > q -> q + (p - q) = p
p, q:BinNums.positive
H:p > q

q + (p - q) = p
p, q:BinNums.positive
H:p > q

p - q + q = p
now apply Pos.sub_add, Pos.gt_lt. Qed.
Discontinued results of little interest and little/zero use in user contributions:
Pplus_carry_no_neutral Pplus_carry_pred_eq_plus Pcompare_not_Eq Pcompare_Lt_Lt Pcompare_Lt_eq_Lt Pcompare_Gt_Gt Pcompare_Gt_eq_Gt Psucc_lt_compat Psucc_le_compat ZC3 Pcompare_p_Sq Pminus_mask_carry_diag Pminus_mask_IsNeg ZL10 ZL11 double_eq_zero_inversion double_plus_one_zero_discr double_plus_one_eq_one_inversion double_eq_one_discr
Infix "/" := Pdiv2 : positive_scope.
Old stuff, to remove someday

forall r : comparison, r = Eq \/ r = Lt \/ r = Gt

forall r : comparison, r = Eq \/ r = Lt \/ r = Gt
destruct r; auto. Qed.
Incompatibilities :