(* -*- 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 Import BinPos PeanoNat.

Local Open Scope positive_scope.
Local Open Scope nat_scope.

Module Pos2Nat.
 Import Pos.

Lemma inj_succ p : to_nat (succ p) = S (to_nat p).
p:positive
to_nat (succ p) = S (to_nat p)
Proof.
p:positive
to_nat (succ p) = S (to_nat p)
 unfold to_nat.
p:positive
iter_op Init.Nat.add (succ p) 1 =
S (iter_op Init.Nat.add p 1) rewrite iter_op_succ.
p:positive
1 + iter_op Init.Nat.add p 1 =
S (iter_op Init.Nat.add p 1)
p:positive
forall x y z : nat, x + (y + z) = x + y + z trivial.
p:positive
forall x y z : nat, x + (y + z) = x + y + z
 apply Nat.add_assoc.
Qed.

Theorem inj_add p q : to_nat (p + q) = to_nat p + to_nat q.
p, q:positive
to_nat (p + q) = to_nat p + to_nat q
Proof.
p, q:positive
to_nat (p + q) = to_nat p + to_nat q
 revert q.
p:positive
forall q : positive,
to_nat (p + q) = to_nat p + to_nat q induction p using peano_ind; intros q.
q:positive
to_nat (1 + q) = to_nat 1 + to_nat q
p:positive
IHp:forall q0 : positive, to_nat (p + q0) = to_nat p + to_nat q0
q:positive
to_nat (succ p + q) = to_nat (succ p) + to_nat q
 now rewrite add_1_l, inj_succ.
p:positive
IHp:forall q0 : positive, to_nat (p + q0) = to_nat p + to_nat q0
q:positive
to_nat (succ p + q) = to_nat (succ p) + to_nat q
 now rewrite add_succ_l, !inj_succ, IHp.
Qed.

Theorem inj_mul p q : to_nat (p * q) = to_nat p * to_nat q.
p, q:positive
to_nat (p * q) = to_nat p * to_nat q
Proof.
p, q:positive
to_nat (p * q) = to_nat p * to_nat q
 revert q.
p:positive
forall q : positive,
to_nat (p * q) = to_nat p * to_nat q induction p using peano_ind; simpl; intros; trivial.
p:positive
IHp:forall q0 : positive, to_nat (p * q0) = to_nat p * to_nat q0
q:positive
to_nat (succ p * q) = to_nat (succ p) * to_nat q
 now rewrite mul_succ_l, inj_add, IHp, inj_succ.
Qed.

Lemma inj_1 : to_nat 1 = 1.
to_nat 1 = 1
Proof.
to_nat 1 = 1
 reflexivity.
Qed.

Lemma inj_xO p : to_nat (xO p) = 2 * to_nat p.
p:positive
to_nat p~0 = 2 * to_nat p
Proof.
p:positive
to_nat p~0 = 2 * to_nat p
 exact (inj_mul 2 p).
Qed.

Lemma inj_xI p : to_nat (xI p) = S (2 * to_nat p).
p:positive
to_nat p~1 = S (2 * to_nat p)
Proof.
p:positive
to_nat p~1 = S (2 * to_nat p)
 now rewrite xI_succ_xO, inj_succ, inj_xO.
Qed.

Lemma is_succ : forall p, exists n, to_nat p = S n.
forall p : positive, exists n : nat, to_nat p = S n
Proof.
forall p : positive, exists n : nat, to_nat p = S n
 induction p using peano_ind.
exists n : nat, to_nat 1 = S n
p:positive
IHp:exists n : nat, to_nat p = S n
exists n : nat, to_nat (succ p) = S n
 now exists 0.
p:positive
IHp:exists n : nat, to_nat p = S n
exists n : nat, to_nat (succ p) = S n
 destruct IHp as (n,Hn).
p:positive
n:nat
Hn:to_nat p = S n
exists n0 : nat, to_nat (succ p) = S n0 exists (S n).
p:positive
n:nat
Hn:to_nat p = S n
to_nat (succ p) = S (S n) now rewrite inj_succ, Hn.
Qed.

Lemma is_pos p : 0 < to_nat p.
p:positive
0 < to_nat p
Proof.
p:positive
0 < to_nat p
 destruct (is_succ p) as (n,->).
p:positive
n:nat
0 < S n auto with arith.
Qed.

Theorem id p : of_nat (to_nat p) = p.
p:positive
of_nat (to_nat p) = p
Proof.
p:positive
of_nat (to_nat p) = p
 induction p using peano_ind.
of_nat (to_nat 1) = 1%positive
p:positive
IHp:of_nat (to_nat p) = p
of_nat (to_nat (succ p)) = succ p trivial.
p:positive
IHp:of_nat (to_nat p) = p
of_nat (to_nat (succ p)) = succ p
 rewrite inj_succ.
p:positive
IHp:of_nat (to_nat p) = p
of_nat (S (to_nat p)) = succ p rewrite <- IHp at 2.
p:positive
IHp:of_nat (to_nat p) = p
of_nat (S (to_nat p)) = succ (of_nat (to_nat p))
 now destruct (is_succ p) as (n,->).
Qed.

Lemma inj p q : to_nat p = to_nat q -> p = q.
p, q:positive
to_nat p = to_nat q -> p = q
Proof.
p, q:positive
to_nat p = to_nat q -> p = q
 intros H.
p, q:positive
H:to_nat p = to_nat q
p = q now rewrite <- (id p), <- (id q), H.
Qed.

Lemma inj_iff p q : to_nat p = to_nat q <-> p = q.
p, q:positive
to_nat p = to_nat q <-> p = q
Proof.
p, q:positive
to_nat p = to_nat q <-> p = q
 split.
p, q:positive
to_nat p = to_nat q -> p = q
p, q:positive
p = q -> to_nat p = to_nat q apply inj.
p, q:positive
p = q -> to_nat p = to_nat q intros; now subst.
Qed.

Lemma inj_compare p q : (p ?= q)%positive = (to_nat p ?= to_nat q).
p, q:positive
(p ?= q)%positive = (to_nat p ?= to_nat q)
Proof.
p, q:positive
(p ?= q)%positive = (to_nat p ?= to_nat q)
 revert q.
p:positive
forall q : positive,
(p ?= q)%positive = (to_nat p ?= to_nat q) induction p as [ |p IH] using peano_ind; intros q.
q:positive
(1 ?= q)%positive = (to_nat 1 ?= to_nat q)
p:positive
IH:forall q0 : positive,
(p ?= q0)%positive = (to_nat p ?= to_nat q0)
q:positive
(succ p ?= q)%positive = (to_nat (succ p) ?= to_nat q)
 -
q:positive
(1 ?= q)%positive = (to_nat 1 ?= to_nat q) destruct (succ_pred_or q) as [Hq|Hq]; [now subst|].
q:positive
Hq:succ (pred q) = q
(1 ?= q)%positive = (to_nat 1 ?= to_nat q)
   rewrite <- Hq, lt_1_succ, inj_succ, inj_1, Nat.compare_succ.
q:positive
Hq:succ (pred q) = q
Lt = (0 ?= to_nat (pred q))
   symmetry.
q:positive
Hq:succ (pred q) = q
(0 ?= to_nat (pred q)) = Lt apply Nat.compare_lt_iff, is_pos.
 -
p:positive
IH:forall q0 : positive,
(p ?= q0)%positive = (to_nat p ?= to_nat q0)
q:positive
(succ p ?= q)%positive = (to_nat (succ p) ?= to_nat q) destruct (succ_pred_or q) as [Hq|Hq]; [subst|].
p:positive
IH:forall q : positive,
(p ?= q)%positive = (to_nat p ?= to_nat q)
(succ p ?= 1)%positive = (to_nat (succ p) ?= to_nat 1)
p:positive
IH:forall q0 : positive,
(p ?= q0)%positive = (to_nat p ?= to_nat q0)
q:positive
Hq:succ (pred q) = q
(succ p ?= q)%positive = (to_nat (succ p) ?= to_nat q)
   rewrite compare_antisym, lt_1_succ, inj_succ.
p:positive
IH:forall q : positive,
(p ?= q)%positive = (to_nat p ?= to_nat q)
CompOpp Lt = (S (to_nat p) ?= to_nat 1)
p:positive
IH:forall q0 : positive,
(p ?= q0)%positive = (to_nat p ?= to_nat q0)
q:positive
Hq:succ (pred q) = q
(succ p ?= q)%positive = (to_nat (succ p) ?= to_nat q) simpl.
p:positive
IH:forall q : positive,
(p ?= q)%positive = (to_nat p ?= to_nat q)
Gt = (to_nat p ?= 0)
p:positive
IH:forall q0 : positive,
(p ?= q0)%positive = (to_nat p ?= to_nat q0)
q:positive
Hq:succ (pred q) = q
(succ p ?= q)%positive = (to_nat (succ p) ?= to_nat q)
   symmetry.
p:positive
IH:forall q : positive,
(p ?= q)%positive = (to_nat p ?= to_nat q)
(to_nat p ?= 0) = Gt
p:positive
IH:forall q0 : positive,
(p ?= q0)%positive = (to_nat p ?= to_nat q0)
q:positive
Hq:succ (pred q) = q
(succ p ?= q)%positive = (to_nat (succ p) ?= to_nat q) apply Nat.compare_gt_iff, is_pos.
p:positive
IH:forall q0 : positive,
(p ?= q0)%positive = (to_nat p ?= to_nat q0)
q:positive
Hq:succ (pred q) = q
(succ p ?= q)%positive = (to_nat (succ p) ?= to_nat q)
   now rewrite <- Hq, 2 inj_succ, compare_succ_succ, IH.
Qed.

Lemma inj_lt p q : (p < q)%positive <-> to_nat p < to_nat q.
p, q:positive
(p < q)%positive <-> to_nat p < to_nat q
Proof.
p, q:positive
(p < q)%positive <-> to_nat p < to_nat q
 unfold lt.
p, q:positive
(p ?= q)%positive = Lt <-> to_nat p < to_nat q now rewrite inj_compare, Nat.compare_lt_iff.
Qed.

Lemma inj_le p q : (p <= q)%positive <-> to_nat p <= to_nat q.
p, q:positive
(p <= q)%positive <-> to_nat p <= to_nat q
Proof.
p, q:positive
(p <= q)%positive <-> to_nat p <= to_nat q
 unfold le.
p, q:positive
(p ?= q)%positive <> Gt <-> to_nat p <= to_nat q now rewrite inj_compare, Nat.compare_le_iff.
Qed.

Lemma inj_gt p q : (p > q)%positive <-> to_nat p > to_nat q.
p, q:positive
(p > q)%positive <-> to_nat p > to_nat q
Proof.
p, q:positive
(p > q)%positive <-> to_nat p > to_nat q
 unfold gt.
p, q:positive
(p ?= q)%positive = Gt <-> to_nat p > to_nat q now rewrite inj_compare, Nat.compare_gt_iff.
Qed.

Lemma inj_ge p q : (p >= q)%positive <-> to_nat p >= to_nat q.
p, q:positive
(p >= q)%positive <-> to_nat p >= to_nat q
Proof.
p, q:positive
(p >= q)%positive <-> to_nat p >= to_nat q
 unfold ge.
p, q:positive
(p ?= q)%positive <> Lt <-> to_nat p >= to_nat q now rewrite inj_compare, Nat.compare_ge_iff.
Qed.

Theorem inj_sub p q : (q < p)%positive ->
 to_nat (p - q) = to_nat p - to_nat q.
p, q:positive
(q < p)%positive ->
to_nat (p - q) = to_nat p - to_nat q
Proof.
p, q:positive
(q < p)%positive ->
to_nat (p - q) = to_nat p - to_nat q
 intro H.
p, q:positive
H:(q < p)%positive
to_nat (p - q) = to_nat p - to_nat q apply Nat.add_cancel_r with (to_nat q).
p, q:positive
H:(q < p)%positive
to_nat (p - q) + to_nat q =
to_nat p - to_nat q + to_nat q
 rewrite Nat.sub_add.
p, q:positive
H:(q < p)%positive
to_nat (p - q) + to_nat q = to_nat p
p, q:positive
H:(q < p)%positive
to_nat q <= to_nat p
 now rewrite <- inj_add, sub_add.
p, q:positive
H:(q < p)%positive
to_nat q <= to_nat p
 now apply Nat.lt_le_incl, inj_lt.
Qed.

Theorem inj_sub_max p q :
 to_nat (p - q) = Nat.max 1 (to_nat p - to_nat q).
p, q:positive
to_nat (p - q) = Nat.max 1 (to_nat p - to_nat q)
Proof.
p, q:positive
to_nat (p - q) = Nat.max 1 (to_nat p - to_nat q)
 destruct (ltb_spec q p).
p, q:positive
H:(q < p)%positive
to_nat (p - q) = Nat.max 1 (to_nat p - to_nat q)
p, q:positive
H:(p <= q)%positive
to_nat (p - q) = Nat.max 1 (to_nat p - to_nat q)
 - (* q < p *)
p, q:positive
H:(q < p)%positive
to_nat (p - q) = Nat.max 1 (to_nat p - to_nat q)
   rewrite <- inj_sub by trivial.
p, q:positive
H:(q < p)%positive
to_nat (p - q) = Nat.max 1 (to_nat (p - q))
   now destruct (is_succ (p - q)) as (m,->).
 - (* p <= q *)
p, q:positive
H:(p <= q)%positive
to_nat (p - q) = Nat.max 1 (to_nat p - to_nat q)
   rewrite sub_le by trivial.
p, q:positive
H:(p <= q)%positive
to_nat 1 = Nat.max 1 (to_nat p - to_nat q)
   apply inj_le, Nat.sub_0_le in H.
p, q:positive
H:to_nat p - to_nat q = 0
to_nat 1 = Nat.max 1 (to_nat p - to_nat q) now rewrite H.
Qed.

Theorem inj_pred p : (1 < p)%positive ->
 to_nat (pred p) = Nat.pred (to_nat p).
p:positive
(1 < p)%positive ->
to_nat (pred p) = Nat.pred (to_nat p)
Proof.
p:positive
(1 < p)%positive ->
to_nat (pred p) = Nat.pred (to_nat p)
 intros.
p:positive
H:(1 < p)%positive
to_nat (pred p) = Nat.pred (to_nat p) now rewrite <- Pos.sub_1_r, inj_sub, Nat.sub_1_r.
Qed.

Theorem inj_pred_max p :
 to_nat (pred p) = Nat.max 1 (Peano.pred (to_nat p)).
p:positive
to_nat (pred p) = Nat.max 1 (Init.Nat.pred (to_nat p))
Proof.
p:positive
to_nat (pred p) = Nat.max 1 (Init.Nat.pred (to_nat p))
 rewrite <- Pos.sub_1_r, <- Nat.sub_1_r.
p:positive
to_nat (p - 1) = Nat.max 1 (to_nat p - 1) apply inj_sub_max.
Qed.

Lemma inj_min p q :
 to_nat (min p q) = Nat.min (to_nat p) (to_nat q).
p, q:positive
to_nat (min p q) = Nat.min (to_nat p) (to_nat q)
Proof.
p, q:positive
to_nat (min p q) = Nat.min (to_nat p) (to_nat q)
 unfold min.
p, q:positive
to_nat
  match (p ?= q)%positive with
  | Gt => q
  | _ => p
  end = Nat.min (to_nat p) (to_nat q) rewrite inj_compare.
p, q:positive
to_nat
  match to_nat p ?= to_nat q with
  | Gt => q
  | _ => p
  end = Nat.min (to_nat p) (to_nat q)
 case Nat.compare_spec; intros H; symmetry.
p, q:positive
H:to_nat p = to_nat q
Nat.min (to_nat p) (to_nat q) = to_nat p
p, q:positive
H:to_nat p < to_nat q
Nat.min (to_nat p) (to_nat q) = to_nat p
p, q:positive
H:to_nat q < to_nat p
Nat.min (to_nat p) (to_nat q) = to_nat q
 -
p, q:positive
H:to_nat p = to_nat q
Nat.min (to_nat p) (to_nat q) = to_nat p apply Nat.min_l.
p, q:positive
H:to_nat p = to_nat q
to_nat p <= to_nat q now rewrite H.
 -
p, q:positive
H:to_nat p < to_nat q
Nat.min (to_nat p) (to_nat q) = to_nat p now apply Nat.min_l, Nat.lt_le_incl.
 -
p, q:positive
H:to_nat q < to_nat p
Nat.min (to_nat p) (to_nat q) = to_nat q now apply Nat.min_r, Nat.lt_le_incl.
Qed.

Lemma inj_max p q :
 to_nat (max p q) = Nat.max (to_nat p) (to_nat q).
p, q:positive
to_nat (max p q) = Nat.max (to_nat p) (to_nat q)
Proof.
p, q:positive
to_nat (max p q) = Nat.max (to_nat p) (to_nat q)
 unfold max.
p, q:positive
to_nat
  match (p ?= q)%positive with
  | Gt => p
  | _ => q
  end = Nat.max (to_nat p) (to_nat q) rewrite inj_compare.
p, q:positive
to_nat
  match to_nat p ?= to_nat q with
  | Gt => p
  | _ => q
  end = Nat.max (to_nat p) (to_nat q)
 case Nat.compare_spec; intros H; symmetry.
p, q:positive
H:to_nat p = to_nat q
Nat.max (to_nat p) (to_nat q) = to_nat q
p, q:positive
H:to_nat p < to_nat q
Nat.max (to_nat p) (to_nat q) = to_nat q
p, q:positive
H:to_nat q < to_nat p
Nat.max (to_nat p) (to_nat q) = to_nat p
 -
p, q:positive
H:to_nat p = to_nat q
Nat.max (to_nat p) (to_nat q) = to_nat q apply Nat.max_r.
p, q:positive
H:to_nat p = to_nat q
to_nat p <= to_nat q now rewrite H.
 -
p, q:positive
H:to_nat p < to_nat q
Nat.max (to_nat p) (to_nat q) = to_nat q now apply Nat.max_r, Nat.lt_le_incl.
 -
p, q:positive
H:to_nat q < to_nat p
Nat.max (to_nat p) (to_nat q) = to_nat p now apply Nat.max_l, Nat.lt_le_incl.
Qed.

Theorem inj_iter :
  forall p {A} (f:A->A) (x:A),
    Pos.iter f x p = nat_rect _ x (fun _ => f) (to_nat p).
forall (p : positive) (A : Type) (f : A -> A) (x : A),
iter f x p =
nat_rect (fun _ : nat => A) x (fun _ : nat => f)
  (to_nat p)
Proof.
forall (p : positive) (A : Type) (f : A -> A) (x : A),
iter f x p =
nat_rect (fun _ : nat => A) x (fun _ : nat => f)
  (to_nat p)
 induction p using peano_ind.
forall (A : Type) (f : A -> A) (x : A),
iter f x 1 =
nat_rect (fun _ : nat => A) x (fun _ : nat => f)
  (to_nat 1)
p:positive
IHp:forall (A : Type) (f : A -> A) (x : A),
iter f x p = nat_rect (fun _ : nat => A) x (fun _ : nat => f) (to_nat p)
forall (A : Type) (f : A -> A) (x : A),
iter f x (succ p) =
nat_rect (fun _ : nat => A) x (fun _ : nat => f)
  (to_nat (succ p))
 -
forall (A : Type) (f : A -> A) (x : A),
iter f x 1 =
nat_rect (fun _ : nat => A) x (fun _ : nat => f)
  (to_nat 1) trivial.
 -
p:positive
IHp:forall (A : Type) (f : A -> A) (x : A),
iter f x p = nat_rect (fun _ : nat => A) x (fun _ : nat => f) (to_nat p)
forall (A : Type) (f : A -> A) (x : A),
iter f x (succ p) =
nat_rect (fun _ : nat => A) x (fun _ : nat => f)
  (to_nat (succ p)) intros.
p:positive
IHp:forall (A0 : Type) (f0 : A0 -> A0) (x0 : A0),
iter f0 x0 p = nat_rect (fun _ : nat => A0) x0 (fun _ : nat => f0) (to_nat p)
A:Type
f:A -> A
x:A
iter f x (succ p) =
nat_rect (fun _ : nat => A) x (fun _ : nat => f)
  (to_nat (succ p)) rewrite inj_succ, iter_succ.
p:positive
IHp:forall (A0 : Type) (f0 : A0 -> A0) (x0 : A0),
iter f0 x0 p = nat_rect (fun _ : nat => A0) x0 (fun _ : nat => f0) (to_nat p)
A:Type
f:A -> A
x:A
f (iter f x p) =
nat_rect (fun _ : nat => A) x (fun _ : nat => f)
  (S (to_nat p)) 
  simpl.
p:positive
IHp:forall (A0 : Type) (f0 : A0 -> A0) (x0 : A0),
iter f0 x0 p = nat_rect (fun _ : nat => A0) x0 (fun _ : nat => f0) (to_nat p)
A:Type
f:A -> A
x:A
f (iter f x p) =
f
  (nat_rect (fun _ : nat => A) x (fun _ : nat => f)
     (to_nat p)) f_equal.
p:positive
IHp:forall (A0 : Type) (f0 : A0 -> A0) (x0 : A0),
iter f0 x0 p = nat_rect (fun _ : nat => A0) x0 (fun _ : nat => f0) (to_nat p)
A:Type
f:A -> A
x:A
iter f x p =
nat_rect (fun _ : nat => A) x (fun _ : nat => f)
  (to_nat p) apply IHp.
Qed.

End Pos2Nat.

Module Nat2Pos.

Theorem id (n:nat) : n<>0 -> Pos.to_nat (Pos.of_nat n) = n.
n:nat
n <> 0 -> Pos.to_nat (Pos.of_nat n) = n
Proof.
n:nat
n <> 0 -> Pos.to_nat (Pos.of_nat n) = n
 induction n as [|n H]; trivial.
0 <> 0 -> Pos.to_nat (Pos.of_nat 0) = 0
n:nat
H:n <> 0 -> Pos.to_nat (Pos.of_nat n) = n
S n <> 0 -> Pos.to_nat (Pos.of_nat (S n)) = S n now destruct 1.
n:nat
H:n <> 0 -> Pos.to_nat (Pos.of_nat n) = n
S n <> 0 -> Pos.to_nat (Pos.of_nat (S n)) = S n
 intros _.
n:nat
H:n <> 0 -> Pos.to_nat (Pos.of_nat n) = n
Pos.to_nat (Pos.of_nat (S n)) = S n simpl Pos.of_nat.
n:nat
H:n <> 0 -> Pos.to_nat (Pos.of_nat n) = n
Pos.to_nat
  match n with
  | 0%nat => 1
  | S _ => Pos.succ (Pos.of_nat n)
  end = S n destruct n.
H:0 <> 0 -> Pos.to_nat (Pos.of_nat 0) = 0
Pos.to_nat 1 = 1
n:nat
H:S n <> 0 -> Pos.to_nat (Pos.of_nat (S n)) = S n
Pos.to_nat (Pos.succ (Pos.of_nat (S n))) = S (S n) trivial.
n:nat
H:S n <> 0 -> Pos.to_nat (Pos.of_nat (S n)) = S n
Pos.to_nat (Pos.succ (Pos.of_nat (S n))) = S (S n)
 rewrite Pos2Nat.inj_succ.
n:nat
H:S n <> 0 -> Pos.to_nat (Pos.of_nat (S n)) = S n
S (Pos.to_nat (Pos.of_nat (S n))) = S (S n) f_equal.
n:nat
H:S n <> 0 -> Pos.to_nat (Pos.of_nat (S n)) = S n
Pos.to_nat (Pos.of_nat (S n)) = S n now apply H.
Qed.

Theorem id_max (n:nat) : Pos.to_nat (Pos.of_nat n) = max 1 n.
n:nat
Pos.to_nat (Pos.of_nat n) = Init.Nat.max 1 n
Proof.
n:nat
Pos.to_nat (Pos.of_nat n) = Init.Nat.max 1 n
 destruct n.
Pos.to_nat (Pos.of_nat 0) = Init.Nat.max 1 0
n:nat
Pos.to_nat (Pos.of_nat (S n)) = Init.Nat.max 1 (S n) trivial.
n:nat
Pos.to_nat (Pos.of_nat (S n)) = Init.Nat.max 1 (S n) now rewrite id.
Qed.

Lemma inj (n m : nat) : n<>0 -> m<>0 -> Pos.of_nat n = Pos.of_nat m -> n = m.
n, m:nat
n <> 0 ->
m <> 0 -> Pos.of_nat n = Pos.of_nat m -> n = m
Proof.
n, m:nat
n <> 0 ->
m <> 0 -> Pos.of_nat n = Pos.of_nat m -> n = m
 intros Hn Hm H.
n, m:nat
Hn:n <> 0
Hm:m <> 0
H:Pos.of_nat n = Pos.of_nat m
n = m now rewrite <- (id n), <- (id m), H.
Qed.

Lemma inj_iff (n m : nat) : n<>0 -> m<>0 ->
 (Pos.of_nat n = Pos.of_nat m <-> n = m).
n, m:nat
n <> 0 ->
m <> 0 -> Pos.of_nat n = Pos.of_nat m <-> n = m
Proof.
n, m:nat
n <> 0 ->
m <> 0 -> Pos.of_nat n = Pos.of_nat m <-> n = m
 split.
n, m:nat
H:n <> 0
H0:m <> 0
Pos.of_nat n = Pos.of_nat m -> n = m
n, m:nat
H:n <> 0
H0:m <> 0
n = m -> Pos.of_nat n = Pos.of_nat m now apply inj.
n, m:nat
H:n <> 0
H0:m <> 0
n = m -> Pos.of_nat n = Pos.of_nat m intros; now subst.
Qed.

Lemma inj_succ (n:nat) : n<>0 -> Pos.of_nat (S n) = Pos.succ (Pos.of_nat n).
n:nat
n <> 0 -> Pos.of_nat (S n) = Pos.succ (Pos.of_nat n)
Proof.
n:nat
n <> 0 -> Pos.of_nat (S n) = Pos.succ (Pos.of_nat n)
intro H.
n:nat
H:n <> 0
Pos.of_nat (S n) = Pos.succ (Pos.of_nat n) apply Pos2Nat.inj.
n:nat
H:n <> 0
Pos.to_nat (Pos.of_nat (S n)) =
Pos.to_nat (Pos.succ (Pos.of_nat n)) now rewrite Pos2Nat.inj_succ, !id.
Qed.

Lemma inj_pred (n:nat) : Pos.of_nat (pred n) = Pos.pred (Pos.of_nat n).
n:nat
Pos.of_nat (Init.Nat.pred n) = Pos.pred (Pos.of_nat n)
Proof.
n:nat
Pos.of_nat (Init.Nat.pred n) = Pos.pred (Pos.of_nat n)
 destruct n as [|[|n]]; trivial.
n:nat
Pos.of_nat (Init.Nat.pred (S (S n))) =
Pos.pred (Pos.of_nat (S (S n))) simpl.
n:nat
match n with
| 0 => 1%positive
| S _ => Pos.succ (Pos.of_nat n)
end =
Pos.pred
  (Pos.succ
     match n with
     | 0%nat => 1
     | S _ => Pos.succ (Pos.of_nat n)
     end) now rewrite Pos.pred_succ.
Qed.

Lemma inj_add (n m : nat) : n<>0 -> m<>0 ->
 Pos.of_nat (n+m) = (Pos.of_nat n + Pos.of_nat m)%positive.
n, m:nat
n <> 0 ->
m <> 0 ->
Pos.of_nat (n + m) =
(Pos.of_nat n + Pos.of_nat m)%positive
Proof.
n, m:nat
n <> 0 ->
m <> 0 ->
Pos.of_nat (n + m) =
(Pos.of_nat n + Pos.of_nat m)%positive
intros Hn Hm.
n, m:nat
Hn:n <> 0
Hm:m <> 0
Pos.of_nat (n + m) =
(Pos.of_nat n + Pos.of_nat m)%positive apply Pos2Nat.inj.
n, m:nat
Hn:n <> 0
Hm:m <> 0
Pos.to_nat (Pos.of_nat (n + m)) =
Pos.to_nat (Pos.of_nat n + Pos.of_nat m)
rewrite Pos2Nat.inj_add, !id; trivial.
n, m:nat
Hn:n <> 0
Hm:m <> 0
n + m <> 0
intros H.
n, m:nat
Hn:n <> 0
Hm:m <> 0
H:n + m = 0
False destruct n.
m:nat
Hn:0 <> 0
Hm:m <> 0
H:0 + m = 0
False
n, m:nat
Hn:S n <> 0
Hm:m <> 0
H:S n + m = 0
False now destruct Hn.
n, m:nat
Hn:S n <> 0
Hm:m <> 0
H:S n + m = 0
False now simpl in H.
Qed.

Lemma inj_mul (n m : nat) : n<>0 -> m<>0 ->
 Pos.of_nat (n*m) = (Pos.of_nat n * Pos.of_nat m)%positive.
n, m:nat
n <> 0 ->
m <> 0 ->
Pos.of_nat (n * m) =
(Pos.of_nat n * Pos.of_nat m)%positive
Proof.
n, m:nat
n <> 0 ->
m <> 0 ->
Pos.of_nat (n * m) =
(Pos.of_nat n * Pos.of_nat m)%positive
intros Hn Hm.
n, m:nat
Hn:n <> 0
Hm:m <> 0
Pos.of_nat (n * m) =
(Pos.of_nat n * Pos.of_nat m)%positive apply Pos2Nat.inj.
n, m:nat
Hn:n <> 0
Hm:m <> 0
Pos.to_nat (Pos.of_nat (n * m)) =
Pos.to_nat (Pos.of_nat n * Pos.of_nat m)
rewrite Pos2Nat.inj_mul, !id; trivial.
n, m:nat
Hn:n <> 0
Hm:m <> 0
n * m <> 0
intros H.
n, m:nat
Hn:n <> 0
Hm:m <> 0
H:n * m = 0
False apply Nat.mul_eq_0 in H.
n, m:nat
Hn:n <> 0
Hm:m <> 0
H:n = 0 \/ m = 0
False destruct H.
n, m:nat
Hn:n <> 0
Hm:m <> 0
H:n = 0
False
n, m:nat
Hn:n <> 0
Hm:m <> 0
H:m = 0
False now elim Hn.
n, m:nat
Hn:n <> 0
Hm:m <> 0
H:m = 0
False now elim Hm.
Qed.

Lemma inj_compare (n m : nat) : n<>0 -> m<>0 ->
 (n ?= m) = (Pos.of_nat n ?= Pos.of_nat m)%positive.
n, m:nat
n <> 0 ->
m <> 0 ->
(n ?= m) = (Pos.of_nat n ?= Pos.of_nat m)%positive
Proof.
n, m:nat
n <> 0 ->
m <> 0 ->
(n ?= m) = (Pos.of_nat n ?= Pos.of_nat m)%positive
intros Hn Hm.
n, m:nat
Hn:n <> 0
Hm:m <> 0
(n ?= m) = (Pos.of_nat n ?= Pos.of_nat m)%positive rewrite Pos2Nat.inj_compare, !id; trivial.
Qed.

Lemma inj_sub (n m : nat) : m<>0 ->
 Pos.of_nat (n-m) = (Pos.of_nat n - Pos.of_nat m)%positive.
n, m:nat
m <> 0 ->
Pos.of_nat (n - m) =
(Pos.of_nat n - Pos.of_nat m)%positive
Proof.
n, m:nat
m <> 0 ->
Pos.of_nat (n - m) =
(Pos.of_nat n - Pos.of_nat m)%positive
 intros Hm.
n, m:nat
Hm:m <> 0
Pos.of_nat (n - m) =
(Pos.of_nat n - Pos.of_nat m)%positive
 apply Pos2Nat.inj.
n, m:nat
Hm:m <> 0
Pos.to_nat (Pos.of_nat (n - m)) =
Pos.to_nat (Pos.of_nat n - Pos.of_nat m)
 rewrite Pos2Nat.inj_sub_max.
n, m:nat
Hm:m <> 0
Pos.to_nat (Pos.of_nat (n - m)) =
Nat.max 1
  (Pos.to_nat (Pos.of_nat n) -
   Pos.to_nat (Pos.of_nat m))
 rewrite (id m) by trivial.
n, m:nat
Hm:m <> 0
Pos.to_nat (Pos.of_nat (n - m)) =
Nat.max 1 (Pos.to_nat (Pos.of_nat n) - m) rewrite !id_max.
n, m:nat
Hm:m <> 0
Init.Nat.max 1 (n - m) =
Nat.max 1 (Init.Nat.max 1 n - m)
 destruct n, m; trivial.
Qed.

Lemma inj_min (n m : nat) :
 Pos.of_nat (min n m) = Pos.min (Pos.of_nat n) (Pos.of_nat m).
n, m:nat
Pos.of_nat (Init.Nat.min n m) =
Pos.min (Pos.of_nat n) (Pos.of_nat m)
Proof.
n, m:nat
Pos.of_nat (Init.Nat.min n m) =
Pos.min (Pos.of_nat n) (Pos.of_nat m)
 destruct n as [|n].
m:nat
Pos.of_nat (Init.Nat.min 0 m) =
Pos.min (Pos.of_nat 0) (Pos.of_nat m)
n, m:nat
Pos.of_nat (Init.Nat.min (S n) m) =
Pos.min (Pos.of_nat (S n)) (Pos.of_nat m) simpl.
m:nat
1%positive = Pos.min 1 (Pos.of_nat m)
n, m:nat
Pos.of_nat (Init.Nat.min (S n) m) =
Pos.min (Pos.of_nat (S n)) (Pos.of_nat m) symmetry.
m:nat
Pos.min 1 (Pos.of_nat m) = 1%positive
n, m:nat
Pos.of_nat (Init.Nat.min (S n) m) =
Pos.min (Pos.of_nat (S n)) (Pos.of_nat m) apply Pos.min_l, Pos.le_1_l.
n, m:nat
Pos.of_nat (Init.Nat.min (S n) m) =
Pos.min (Pos.of_nat (S n)) (Pos.of_nat m)
 destruct m as [|m].
n:nat
Pos.of_nat (Init.Nat.min (S n) 0) =
Pos.min (Pos.of_nat (S n)) (Pos.of_nat 0)
n, m:nat
Pos.of_nat (Init.Nat.min (S n) (S m)) =
Pos.min (Pos.of_nat (S n)) (Pos.of_nat (S m)) simpl.
n:nat
1%positive =
Pos.min
  match n with
  | 0%nat => 1
  | S _ => Pos.succ (Pos.of_nat n)
  end 1
n, m:nat
Pos.of_nat (Init.Nat.min (S n) (S m)) =
Pos.min (Pos.of_nat (S n)) (Pos.of_nat (S m)) symmetry.
n:nat
Pos.min
  match n with
  | 0%nat => 1
  | S _ => Pos.succ (Pos.of_nat n)
  end 1 = 1%positive
n, m:nat
Pos.of_nat (Init.Nat.min (S n) (S m)) =
Pos.min (Pos.of_nat (S n)) (Pos.of_nat (S m)) apply Pos.min_r, Pos.le_1_l.
n, m:nat
Pos.of_nat (Init.Nat.min (S n) (S m)) =
Pos.min (Pos.of_nat (S n)) (Pos.of_nat (S m))
 unfold Pos.min.
n, m:nat
Pos.of_nat (Init.Nat.min (S n) (S m)) =
match
  (Pos.of_nat (S n) ?= Pos.of_nat (S m))%positive
with
| Gt => Pos.of_nat (S m)
| _ => Pos.of_nat (S n)
end rewrite <- inj_compare by easy.
n, m:nat
Pos.of_nat (Init.Nat.min (S n) (S m)) =
match S n ?= S m with
| Gt => Pos.of_nat (S m)
| _ => Pos.of_nat (S n)
end
 case Nat.compare_spec; intros H; f_equal;
  apply Nat.min_l || apply Nat.min_r.
n, m:nat
H:S n = S m
S n <= S m
n, m:nat
H:S n < S m
S n <= S m
n, m:nat
H:S m < S n
S m <= S n
 rewrite H; auto.
n, m:nat
H:S n < S m
S n <= S m
n, m:nat
H:S m < S n
S m <= S n now apply Nat.lt_le_incl.
n, m:nat
H:S m < S n
S m <= S n now apply Nat.lt_le_incl.
Qed.

Lemma inj_max (n m : nat) :
 Pos.of_nat (max n m) = Pos.max (Pos.of_nat n) (Pos.of_nat m).
n, m:nat
Pos.of_nat (Init.Nat.max n m) =
Pos.max (Pos.of_nat n) (Pos.of_nat m)
Proof.
n, m:nat
Pos.of_nat (Init.Nat.max n m) =
Pos.max (Pos.of_nat n) (Pos.of_nat m)
 destruct n as [|n].
m:nat
Pos.of_nat (Init.Nat.max 0 m) =
Pos.max (Pos.of_nat 0) (Pos.of_nat m)
n, m:nat
Pos.of_nat (Init.Nat.max (S n) m) =
Pos.max (Pos.of_nat (S n)) (Pos.of_nat m) simpl.
m:nat
Pos.of_nat m = Pos.max 1 (Pos.of_nat m)
n, m:nat
Pos.of_nat (Init.Nat.max (S n) m) =
Pos.max (Pos.of_nat (S n)) (Pos.of_nat m) symmetry.
m:nat
Pos.max 1 (Pos.of_nat m) = Pos.of_nat m
n, m:nat
Pos.of_nat (Init.Nat.max (S n) m) =
Pos.max (Pos.of_nat (S n)) (Pos.of_nat m) apply Pos.max_r, Pos.le_1_l.
n, m:nat
Pos.of_nat (Init.Nat.max (S n) m) =
Pos.max (Pos.of_nat (S n)) (Pos.of_nat m)
 destruct m as [|m].
n:nat
Pos.of_nat (Init.Nat.max (S n) 0) =
Pos.max (Pos.of_nat (S n)) (Pos.of_nat 0)
n, m:nat
Pos.of_nat (Init.Nat.max (S n) (S m)) =
Pos.max (Pos.of_nat (S n)) (Pos.of_nat (S m)) simpl.
n:nat
match n with
| 0 => 1%positive
| S _ => Pos.succ (Pos.of_nat n)
end =
Pos.max
  match n with
  | 0%nat => 1
  | S _ => Pos.succ (Pos.of_nat n)
  end 1
n, m:nat
Pos.of_nat (Init.Nat.max (S n) (S m)) =
Pos.max (Pos.of_nat (S n)) (Pos.of_nat (S m)) symmetry.
n:nat
Pos.max
  match n with
  | 0%nat => 1
  | S _ => Pos.succ (Pos.of_nat n)
  end 1 =
match n with
| 0 => 1%positive
| S _ => Pos.succ (Pos.of_nat n)
end
n, m:nat
Pos.of_nat (Init.Nat.max (S n) (S m)) =
Pos.max (Pos.of_nat (S n)) (Pos.of_nat (S m)) apply Pos.max_l, Pos.le_1_l.
n, m:nat
Pos.of_nat (Init.Nat.max (S n) (S m)) =
Pos.max (Pos.of_nat (S n)) (Pos.of_nat (S m))
 unfold Pos.max.
n, m:nat
Pos.of_nat (Init.Nat.max (S n) (S m)) =
match
  (Pos.of_nat (S n) ?= Pos.of_nat (S m))%positive
with
| Gt => Pos.of_nat (S n)
| _ => Pos.of_nat (S m)
end rewrite <- inj_compare by easy.
n, m:nat
Pos.of_nat (Init.Nat.max (S n) (S m)) =
match S n ?= S m with
| Gt => Pos.of_nat (S n)
| _ => Pos.of_nat (S m)
end
 case Nat.compare_spec; intros H; f_equal;
  apply Nat.max_l || apply Nat.max_r.
n, m:nat
H:S n = S m
S n <= S m
n, m:nat
H:S n < S m
S n <= S m
n, m:nat
H:S m < S n
S m <= S n
 rewrite H; auto.
n, m:nat
H:S n < S m
S n <= S m
n, m:nat
H:S m < S n
S m <= S n now apply Nat.lt_le_incl.
n, m:nat
H:S m < S n
S m <= S n now apply Nat.lt_le_incl.
Qed.

End Nat2Pos.

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

Module Pos2SuccNat.

Theorem id_succ p : Pos.of_succ_nat (Pos.to_nat p) = Pos.succ p.
p:positive
Pos.of_succ_nat (Pos.to_nat p) = Pos.succ p
Proof.
p:positive
Pos.of_succ_nat (Pos.to_nat p) = Pos.succ p
rewrite Pos.of_nat_succ, <- Pos2Nat.inj_succ.
p:positive
Pos.of_nat (Pos.to_nat (Pos.succ p)) = Pos.succ p apply Pos2Nat.id.
Qed.

Theorem pred_id p : Pos.pred (Pos.of_succ_nat (Pos.to_nat p)) = p.
p:positive
Pos.pred (Pos.of_succ_nat (Pos.to_nat p)) = p
Proof.
p:positive
Pos.pred (Pos.of_succ_nat (Pos.to_nat p)) = p
now rewrite id_succ, Pos.pred_succ.
Qed.

End Pos2SuccNat.

Module SuccNat2Pos.

Theorem id_succ (n:nat) : Pos.to_nat (Pos.of_succ_nat n) = S n.
n:nat
Pos.to_nat (Pos.of_succ_nat n) = S n
Proof.
n:nat
Pos.to_nat (Pos.of_succ_nat n) = S n
rewrite Pos.of_nat_succ.
n:nat
Pos.to_nat (Pos.of_nat (S n)) = S n now apply Nat2Pos.id.
Qed.

Theorem pred_id (n:nat) : pred (Pos.to_nat (Pos.of_succ_nat n)) = n.
n:nat
Init.Nat.pred (Pos.to_nat (Pos.of_succ_nat n)) = n
Proof.
n:nat
Init.Nat.pred (Pos.to_nat (Pos.of_succ_nat n)) = n
now rewrite id_succ.
Qed.

Lemma inj (n m : nat) : Pos.of_succ_nat n = Pos.of_succ_nat m -> n = m.
n, m:nat
Pos.of_succ_nat n = Pos.of_succ_nat m -> n = m
Proof.
n, m:nat
Pos.of_succ_nat n = Pos.of_succ_nat m -> n = m
 intro H.
n, m:nat
H:Pos.of_succ_nat n = Pos.of_succ_nat m
n = m apply (f_equal Pos.to_nat) in H.
n, m:nat
H:Pos.to_nat (Pos.of_succ_nat n) =
Pos.to_nat (Pos.of_succ_nat m)
n = m rewrite !id_succ in H.
n, m:nat
H:S n = S m
n = m
 now injection H.
Qed.

Lemma inj_iff (n m : nat) : Pos.of_succ_nat n = Pos.of_succ_nat m <-> n = m.
n, m:nat
Pos.of_succ_nat n = Pos.of_succ_nat m <-> n = m
Proof.
n, m:nat
Pos.of_succ_nat n = Pos.of_succ_nat m <-> n = m
 split.
n, m:nat
Pos.of_succ_nat n = Pos.of_succ_nat m -> n = m
n, m:nat
n = m -> Pos.of_succ_nat n = Pos.of_succ_nat m apply inj.
n, m:nat
n = m -> Pos.of_succ_nat n = Pos.of_succ_nat m intros; now subst.
Qed.

Theorem inv n p : Pos.to_nat p = S n -> Pos.of_succ_nat n = p.
n:nat
p:positive
Pos.to_nat p = S n -> Pos.of_succ_nat n = p
Proof.
n:nat
p:positive
Pos.to_nat p = S n -> Pos.of_succ_nat n = p
 intros H.
n:nat
p:positive
H:Pos.to_nat p = S n
Pos.of_succ_nat n = p apply Pos2Nat.inj.
n:nat
p:positive
H:Pos.to_nat p = S n
Pos.to_nat (Pos.of_succ_nat n) = Pos.to_nat p now rewrite id_succ.
Qed.

Lemma inj_succ n : Pos.of_succ_nat (S n) = Pos.succ (Pos.of_succ_nat n).
n:nat
Pos.of_succ_nat (S n) = Pos.succ (Pos.of_succ_nat n)
Proof.
n:nat
Pos.of_succ_nat (S n) = Pos.succ (Pos.of_succ_nat n)
apply Pos2Nat.inj.
n:nat
Pos.to_nat (Pos.of_succ_nat (S n)) =
Pos.to_nat (Pos.succ (Pos.of_succ_nat n)) now rewrite Pos2Nat.inj_succ, !id_succ.
Qed.

Lemma inj_compare n m :
 (n ?= m) = (Pos.of_succ_nat n ?= Pos.of_succ_nat m)%positive.
n, m:nat
(n ?= m) =
(Pos.of_succ_nat n ?= Pos.of_succ_nat m)%positive
Proof.
n, m:nat
(n ?= m) =
(Pos.of_succ_nat n ?= Pos.of_succ_nat m)%positive
rewrite Pos2Nat.inj_compare, !id_succ; trivial.
Qed.

End SuccNat2Pos.

Notation Psucc_S := Pos2Nat.inj_succ (only parsing).
Notation Pplus_plus := Pos2Nat.inj_add (only parsing).
Notation Pmult_mult := Pos2Nat.inj_mul (only parsing).
Notation Pcompare_nat_compare := Pos2Nat.inj_compare (only parsing).
Notation nat_of_P_xH := Pos2Nat.inj_1 (only parsing).
Notation nat_of_P_xO := Pos2Nat.inj_xO (only parsing).
Notation nat_of_P_xI := Pos2Nat.inj_xI (only parsing).
Notation nat_of_P_is_S := Pos2Nat.is_succ (only parsing).
Notation nat_of_P_pos := Pos2Nat.is_pos (only parsing).
Notation nat_of_P_inj_iff := Pos2Nat.inj_iff (only parsing).
Notation nat_of_P_inj := Pos2Nat.inj (only parsing).
Notation Plt_lt := Pos2Nat.inj_lt (only parsing).
Notation Pgt_gt := Pos2Nat.inj_gt (only parsing).
Notation Ple_le := Pos2Nat.inj_le (only parsing).
Notation Pge_ge := Pos2Nat.inj_ge (only parsing).
Notation Pminus_minus := Pos2Nat.inj_sub (only parsing).
Notation iter_nat_of_P := @Pos2Nat.inj_iter (only parsing).

Notation nat_of_P_of_succ_nat := SuccNat2Pos.id_succ (only parsing).
Notation P_of_succ_nat_of_P := Pos2SuccNat.id_succ (only parsing).

Notation nat_of_P_succ_morphism := Pos2Nat.inj_succ (only parsing).
Notation nat_of_P_plus_morphism := Pos2Nat.inj_add (only parsing).
Notation nat_of_P_mult_morphism := Pos2Nat.inj_mul (only parsing).
Notation nat_of_P_compare_morphism := Pos2Nat.inj_compare (only parsing).
Notation lt_O_nat_of_P := Pos2Nat.is_pos (only parsing).
Notation ZL4 := Pos2Nat.is_succ (only parsing).
Notation nat_of_P_o_P_of_succ_nat_eq_succ := SuccNat2Pos.id_succ (only parsing).
Notation P_of_succ_nat_o_nat_of_P_eq_succ := Pos2SuccNat.id_succ (only parsing).
Notation pred_o_P_of_succ_nat_o_nat_of_P_eq_id := Pos2SuccNat.pred_id (only parsing).

Lemma nat_of_P_minus_morphism p q :
 Pos.compare_cont Eq p q = Gt ->
  Pos.to_nat (p - q) = Pos.to_nat p - Pos.to_nat q.
p, q:positive
Pos.compare_cont Eq p q = Gt ->
Pos.to_nat (p - q) = Pos.to_nat p - Pos.to_nat q
Proof (fun H => Pos2Nat.inj_sub p q (Pos.gt_lt _ _ H)).

Lemma nat_of_P_lt_Lt_compare_morphism p q :
 Pos.compare_cont Eq p q = Lt -> Pos.to_nat p < Pos.to_nat q.
p, q:positive
Pos.compare_cont Eq p q = Lt ->
Pos.to_nat p < Pos.to_nat q
Proof (proj1 (Pos2Nat.inj_lt p q)).

Lemma nat_of_P_gt_Gt_compare_morphism p q :
 Pos.compare_cont Eq p q = Gt -> Pos.to_nat p > Pos.to_nat q.
p, q:positive
Pos.compare_cont Eq p q = Gt ->
Pos.to_nat p > Pos.to_nat q
Proof (proj1 (Pos2Nat.inj_gt p q)).

Lemma nat_of_P_lt_Lt_compare_complement_morphism p q :
 Pos.to_nat p < Pos.to_nat q -> Pos.compare_cont Eq p q = Lt.
p, q:positive
Pos.to_nat p < Pos.to_nat q ->
Pos.compare_cont Eq p q = Lt
Proof (proj2 (Pos2Nat.inj_lt p q)).

Definition nat_of_P_gt_Gt_compare_complement_morphism p q :
 Pos.to_nat p > Pos.to_nat q -> Pos.compare_cont Eq p q = Gt.
p, q:positive
Pos.to_nat p > Pos.to_nat q ->
Pos.compare_cont Eq p q = Gt
Proof (proj2 (Pos2Nat.inj_gt p q)).