Require Import Basics.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Spaces.Pos.
Require Import Spaces.Int.Core.

Local Set Universe Minimization ToSet.

Local Open Scope int_scope.

(** ** Addition is commutative *)

Lemma int_add_comm n m : n + m = m + n.
n, m: Int
n + m = m + n
Proof.
n, m: Int
n + m = m + n
  destruct n, m; trivial.
p, p0: Pos
neg p + neg p0 = neg p0 + neg p
p, p0: Pos
pos p + pos p0 = pos p0 + pos p all: cbn.
p, p0: Pos
neg (p + p0)%pos = neg (p0 + p)%pos
p, p0: Pos
pos (p + p0) = pos (p0 + p)
  all: apply ap, pos_add_comm.
Defined.

(** ** Zero is the additive identity. *)

Definition int_add_0_l n : 0 + n = n
  := 1.

Lemma int_add_0_r n : n + 0 = n.
n: Int
n + 0 = n
Proof.
n: Int
n + 0 = n
  by destruct n.
Defined.

(** ** Multiplication by zero is zero *)

Definition int_mul_0_l n : 0 * n = 0
  := 1.

Lemma int_mul_0_r n : n * 0 = 0.
n: Int
n * 0 = 0
Proof.
n: Int
n * 0 = 0
  by destruct n.
Defined.

(** ** One is the multiplicative identity *)

Lemma int_mul_1_l n : 1 * n = n.
n: Int
1 * n = n
Proof.
n: Int
1 * n = n
  by destruct n.
Defined.

Lemma int_mul_1_r n : n * 1 = n.
n: Int
n * 1 = n
Proof.
n: Int
n * 1 = n
  destruct n; trivial; cbn; apply ap, pos_mul_1_r.
Defined.

(** ** Inverse laws *)

Lemma int_pos_sub_diag n : int_pos_sub n n = 0.
n: Pos
int_pos_sub n n = 0
Proof.
n: Pos
int_pos_sub n n = 0
  induction n; trivial; cbn.
n: Pos
IHn: int_pos_sub n n = 0
int_double (int_pos_sub n n) = 0
n: Pos
IHn: int_pos_sub n n = 0
int_double (int_pos_sub n n) = 0
  all: exact (ap int_double IHn).
Defined.

Lemma int_add_negation_l n : (-n) + n = 0.
n: Int
- n + n = 0
Proof.
n: Int
- n + n = 0
  destruct n; trivial; cbn; apply int_pos_sub_diag.
Defined.

Lemma int_add_negation_r n : n + (-n) = 0.
n: Int
n + - n = 0
Proof.
n: Int
n + - n = 0
  destruct n; trivial; cbn; apply int_pos_sub_diag.
Defined.

(** ** Permutation of neg and pos_succ *)
Lemma int_neg_pos_succ p : neg (pos_succ p) = int_pred (neg p).
p: Pos
neg (pos_succ p) = int_pred (neg p)
Proof.
p: Pos
neg (pos_succ p) = int_pred (neg p)
  by destruct p.
Defined.

(** ** Permutation of pos and pos_succ *)
Lemma int_pos_pos_succ p : pos (pos_succ p) = int_succ (pos p).
p: Pos
pos (pos_succ p) = int_succ (pos p)
Proof.
p: Pos
pos (pos_succ p) = int_succ (pos p)
  by destruct p.
Defined.

(** ** Negation of a doubled positive integer *)
Lemma int_negation_double a : - (int_double a) = int_double (- a).
a: Int
- int_double a = int_double (- a)
Proof.
a: Int
- int_double a = int_double (- a)
  by destruct a.
Defined.

(** Negation of the predecessor of a doubled positive integer. *)
Lemma int_negation_pred_double a : - (int_pred_double a) = int_succ_double (- a).
a: Int
- int_pred_double a = int_succ_double (- a)
Proof.
a: Int
- int_pred_double a = int_succ_double (- a)
  by destruct a.
Defined.

(** Negation of the doubling of the sucessor of an positive. *)
Lemma int_negation_succ_double a : - (int_succ_double a) = int_pred_double (- a).
a: Int
- int_succ_double a = int_pred_double (- a)
Proof.
a: Int
- int_succ_double a = int_pred_double (- a)
  by destruct a.
Defined.

(** Negation of subtraction of positive integers *)
Lemma int_pos_sub_negation a b : - (int_pos_sub a b) = int_pos_sub b a.
a, b: Pos
- int_pos_sub a b = int_pos_sub b a
Proof.
a, b: Pos
- int_pos_sub a b = int_pos_sub b a
  revert a b.
forall a b : Pos, - int_pos_sub a b = int_pos_sub b a
  induction a as [|a ah|a ah];
  destruct b;
  cbn; trivial.
a: Pos
ah: forall b : Pos,
- int_pos_sub a b = int_pos_sub b a
b: Pos
- int_double (int_pos_sub a b) =
int_double (int_pos_sub b a)
a: Pos
ah: forall b : Pos,
- int_pos_sub a b = int_pos_sub b a
b: Pos
- int_pred_double (int_pos_sub a b) =
int_succ_double (int_pos_sub b a)
a: Pos
ah: forall b : Pos,
- int_pos_sub a b = int_pos_sub b a
b: Pos
- int_succ_double (int_pos_sub a b) =
int_pred_double (int_pos_sub b a)
a: Pos
ah: forall b : Pos,
- int_pos_sub a b = int_pos_sub b a
b: Pos
- int_double (int_pos_sub a b) =
int_double (int_pos_sub b a)
  all: rewrite ?int_negation_double,
    ?int_negation_succ_double,
    ?int_negation_pred_double.
a: Pos
ah: forall b : Pos,
- int_pos_sub a b = int_pos_sub b a
b: Pos
int_double (- int_pos_sub a b) =
int_double (int_pos_sub b a)
a: Pos
ah: forall b : Pos,
- int_pos_sub a b = int_pos_sub b a
b: Pos
int_succ_double (- int_pos_sub a b) =
int_succ_double (int_pos_sub b a)
a: Pos
ah: forall b : Pos,
- int_pos_sub a b = int_pos_sub b a
b: Pos
int_pred_double (- int_pos_sub a b) =
int_pred_double (int_pos_sub b a)
a: Pos
ah: forall b : Pos,
- int_pos_sub a b = int_pos_sub b a
b: Pos
int_double (- int_pos_sub a b) =
int_double (int_pos_sub b a)
  all: apply ap, ah.
Defined.

(** ** int_succ is a retract of int_pred *)
Definition int_succ_pred : int_succ o int_pred == idmap.
int_succ o int_pred == idmap
Proof.
int_succ o int_pred == idmap
  intros [n | | n]; [|trivial|].
n: Pos
int_succ (int_pred (neg n)) = neg n
n: Pos
int_succ (int_pred (pos n)) = pos n
  all: destruct n; trivial.
n: Pos
int_succ (int_pred (neg (n~1)%pos)) = neg (n~1)%pos
n: Pos
int_succ (int_pred (pos n~0)) = pos n~0
  1,2: cbn; apply ap.
n: Pos
pos_pred_double (pos_succ n) = (n~1)%pos
n: Pos
(pos_pred_double n + 1)%pos = (n~0)%pos
  1: apply pos_pred_double_succ.
n: Pos
(pos_pred_double n + 1)%pos = (n~0)%pos
  rewrite pos_add_1_r.
n: Pos
pos_succ (pos_pred_double n) = (n~0)%pos
  apply pos_succ_pred_double.
Defined.

(** ** int_pred is a retract of int_succ *)
Definition int_pred_succ : int_pred o int_succ == idmap.
int_pred o int_succ == idmap
Proof.
int_pred o int_succ == idmap
  intros [n | | n]; [|trivial|].
n: Pos
int_pred (int_succ (neg n)) = neg n
n: Pos
int_pred (int_succ (pos n)) = pos n
  all: destruct n; trivial.
n: Pos
int_pred (int_succ (neg (n~0)%pos)) = neg (n~0)%pos
n: Pos
int_pred (int_succ (pos n~1)) = pos n~1
  1,2: cbn; apply ap.
n: Pos
(pos_pred_double n + 1)%pos = (n~0)%pos
n: Pos
pos_pred_double (pos_succ n) = (n~1)%pos
  1: rewrite pos_add_1_r.
n: Pos
pos_succ (pos_pred_double n) = (n~0)%pos
n: Pos
pos_pred_double (pos_succ n) = (n~1)%pos
  1: apply pos_succ_pred_double.
n: Pos
pos_pred_double (pos_succ n) = (n~1)%pos
  apply pos_pred_double_succ.
Defined.

(* ** The successor autoequivalence. *)
Global Instance isequiv_int_succ : IsEquiv int_succ | 0
  := isequiv_adjointify int_succ _ int_succ_pred int_pred_succ.

Definition equiv_int_succ : Int <~> Int
  := Build_Equiv _ _ _ isequiv_int_succ.

(** ** Negation distributes over addition *)
Lemma int_negation_add_distr n m : - (n + m) = - n + - m.
n, m: Int
- (n + m) = - n + - m
Proof.
n, m: Int
- (n + m) = - n + - m
 destruct n, m; simpl; trivial using int_pos_sub_negation.
Defined.

(** ** Negation is injective *)
Lemma int_negation_inj n m : -n = -m -> n = m.
n, m: Int
- n = - m -> n = m
Proof.
n, m: Int
- n = - m -> n = m
  destruct n, m; simpl; intro H.
p, p0: Pos
H: pos p = pos p0
neg p = neg p0
p: Pos
H: pos p = 0
neg p = 0
p, p0: Pos
H: pos p = neg p0
neg p = pos p0
p: Pos
H: 0 = pos p
0 = neg p
H: 0 = 0
0 = 0
p: Pos
H: 0 = neg p
0 = pos p
p, p0: Pos
H: neg p = pos p0
pos p = neg p0
p: Pos
H: neg p = 0
pos p = 0
p, p0: Pos
H: neg p = neg p0
pos p = pos p0
  1: apply pos_inj in H.
p, p0: Pos
H: p = p0
neg p = neg p0
p: Pos
H: pos p = 0
neg p = 0
p, p0: Pos
H: pos p = neg p0
neg p = pos p0
p: Pos
H: 0 = pos p
0 = neg p
H: 0 = 0
0 = 0
p: Pos
H: 0 = neg p
0 = pos p
p, p0: Pos
H: neg p = pos p0
pos p = neg p0
p: Pos
H: neg p = 0
pos p = 0
p, p0: Pos
H: neg p = neg p0
pos p = pos p0
  2: apply pos_neq_zero in H.
p, p0: Pos
H: p = p0
neg p = neg p0
p: Pos
H: Empty
neg p = 0
p, p0: Pos
H: pos p = neg p0
neg p = pos p0
p: Pos
H: 0 = pos p
0 = neg p
H: 0 = 0
0 = 0
p: Pos
H: 0 = neg p
0 = pos p
p, p0: Pos
H: neg p = pos p0
pos p = neg p0
p: Pos
H: neg p = 0
pos p = 0
p, p0: Pos
H: neg p = neg p0
pos p = pos p0
  3: apply pos_neq_neg in H.
p, p0: Pos
H: p = p0
neg p = neg p0
p: Pos
H: Empty
neg p = 0
p, p0: Pos
H: Empty
neg p = pos p0
p: Pos
H: 0 = pos p
0 = neg p
H: 0 = 0
0 = 0
p: Pos
H: 0 = neg p
0 = pos p
p, p0: Pos
H: neg p = pos p0
pos p = neg p0
p: Pos
H: neg p = 0
pos p = 0
p, p0: Pos
H: neg p = neg p0
pos p = pos p0
  4: apply  zero_neq_pos in H.
p, p0: Pos
H: p = p0
neg p = neg p0
p: Pos
H: Empty
neg p = 0
p, p0: Pos
H: Empty
neg p = pos p0
p: Pos
H: Empty
0 = neg p
H: 0 = 0
0 = 0
p: Pos
H: 0 = neg p
0 = pos p
p, p0: Pos
H: neg p = pos p0
pos p = neg p0
p: Pos
H: neg p = 0
pos p = 0
p, p0: Pos
H: neg p = neg p0
pos p = pos p0
  6: apply  zero_neq_neg in H.
p, p0: Pos
H: p = p0
neg p = neg p0
p: Pos
H: Empty
neg p = 0
p, p0: Pos
H: Empty
neg p = pos p0
p: Pos
H: Empty
0 = neg p
H: 0 = 0
0 = 0
p: Pos
H: Empty
0 = pos p
p, p0: Pos
H: neg p = pos p0
pos p = neg p0
p: Pos
H: neg p = 0
pos p = 0
p, p0: Pos
H: neg p = neg p0
pos p = pos p0
  7: apply  neg_neq_pos in H.
p, p0: Pos
H: p = p0
neg p = neg p0
p: Pos
H: Empty
neg p = 0
p, p0: Pos
H: Empty
neg p = pos p0
p: Pos
H: Empty
0 = neg p
H: 0 = 0
0 = 0
p: Pos
H: Empty
0 = pos p
p, p0: Pos
H: Empty
pos p = neg p0
p: Pos
H: neg p = 0
pos p = 0
p, p0: Pos
H: neg p = neg p0
pos p = pos p0
  8: apply  neg_neq_zero in H.
p, p0: Pos
H: p = p0
neg p = neg p0
p: Pos
H: Empty
neg p = 0
p, p0: Pos
H: Empty
neg p = pos p0
p: Pos
H: Empty
0 = neg p
H: 0 = 0
0 = 0
p: Pos
H: Empty
0 = pos p
p, p0: Pos
H: Empty
pos p = neg p0
p: Pos
H: Empty
pos p = 0
p, p0: Pos
H: neg p = neg p0
pos p = pos p0
  9: apply  neg_inj in H.
p, p0: Pos
H: p = p0
neg p = neg p0
p: Pos
H: Empty
neg p = 0
p, p0: Pos
H: Empty
neg p = pos p0
p: Pos
H: Empty
0 = neg p
H: 0 = 0
0 = 0
p: Pos
H: Empty
0 = pos p
p, p0: Pos
H: Empty
pos p = neg p0
p: Pos
H: Empty
pos p = 0
p, p0: Pos
H: p = p0
pos p = pos p0
  all: by destruct H.
Defined.

(** ** Subtracting 1 from a sucessor gives the positive integer. *)
Lemma int_pos_sub_succ_l a
  : int_pos_sub (pos_succ a) 1%pos = pos a.
a: Pos
int_pos_sub (pos_succ a) 1%pos = pos a
Proof.
a: Pos
int_pos_sub (pos_succ a) 1%pos = pos a
  destruct a; trivial.
a: Pos
int_pos_sub (pos_succ (a~1)%pos) 1%pos = pos a~1
  cbn; apply ap, pos_pred_double_succ.
Defined.

(** ** Subtracting a sucessor from 1 gives minus the integer. *)
Lemma int_pos_sub_succ_r a
  : int_pos_sub 1%pos (pos_succ a) = neg a.
a: Pos
int_pos_sub 1%pos (pos_succ a) = neg a
Proof.
a: Pos
int_pos_sub 1%pos (pos_succ a) = neg a
  destruct a; trivial.
a: Pos
int_pos_sub 1%pos (pos_succ (a~1)%pos) = neg (a~1)%pos
  cbn; apply ap, pos_pred_double_succ.
Defined.

(** ** Interaction of doubling functions and subtraction *)

Lemma int_succ_double_int_pos_sub a b
  : int_succ_double (int_pos_sub a (pos_succ b))
    = int_pred_double (int_pos_sub a b).
a, b: Pos
int_succ_double (int_pos_sub a (pos_succ b)) =
int_pred_double (int_pos_sub a b)
Proof.
a, b: Pos
int_succ_double (int_pos_sub a (pos_succ b)) =
int_pred_double (int_pos_sub a b)
  revert a b.
forall a b : Pos,
int_succ_double (int_pos_sub a (pos_succ b)) =
int_pred_double (int_pos_sub a b)
  induction a; induction b; trivial.
b: Pos
IHb: int_succ_double (int_pos_sub 1%pos (pos_succ b)) =
int_pred_double (int_pos_sub 1%pos b)
int_succ_double
  (int_pos_sub 1%pos (pos_succ (b~1)%pos)) =
int_pred_double (int_pos_sub 1%pos (b~1)%pos)
a: Pos
IHa: forall b : Pos,
int_succ_double (int_pos_sub a (pos_succ b)) =
int_pred_double (int_pos_sub a b)
int_succ_double
  (int_pos_sub (a~0)%pos (pos_succ 1%pos)) =
int_pred_double (int_pos_sub (a~0)%pos 1%pos)
a: Pos
IHa: forall b : Pos,
int_succ_double (int_pos_sub a (pos_succ b)) =
int_pred_double (int_pos_sub a b)
b: Pos
IHb: int_succ_double (int_pos_sub (a~0)%pos (pos_succ b)) =
int_pred_double (int_pos_sub (a~0)%pos b)
int_succ_double
  (int_pos_sub (a~0)%pos (pos_succ (b~0)%pos)) =
int_pred_double (int_pos_sub (a~0)%pos (b~0)%pos)
a: Pos
IHa: forall b : Pos,
int_succ_double (int_pos_sub a (pos_succ b)) =
int_pred_double (int_pos_sub a b)
b: Pos
IHb: int_succ_double (int_pos_sub (a~0)%pos (pos_succ b)) =
int_pred_double (int_pos_sub (a~0)%pos b)
int_succ_double
  (int_pos_sub (a~0)%pos (pos_succ (b~1)%pos)) =
int_pred_double (int_pos_sub (a~0)%pos (b~1)%pos)
a: Pos
IHa: forall b : Pos,
int_succ_double (int_pos_sub a (pos_succ b)) =
int_pred_double (int_pos_sub a b)
int_succ_double
  (int_pos_sub (a~1)%pos (pos_succ 1%pos)) =
int_pred_double (int_pos_sub (a~1)%pos 1%pos)
a: Pos
IHa: forall b : Pos,
int_succ_double (int_pos_sub a (pos_succ b)) =
int_pred_double (int_pos_sub a b)
b: Pos
IHb: int_succ_double (int_pos_sub (a~1)%pos (pos_succ b)) =
int_pred_double (int_pos_sub (a~1)%pos b)
int_succ_double
  (int_pos_sub (a~1)%pos (pos_succ (b~0)%pos)) =
int_pred_double (int_pos_sub (a~1)%pos (b~0)%pos)
a: Pos
IHa: forall b : Pos,
int_succ_double (int_pos_sub a (pos_succ b)) =
int_pred_double (int_pos_sub a b)
b: Pos
IHb: int_succ_double (int_pos_sub (a~1)%pos (pos_succ b)) =
int_pred_double (int_pos_sub (a~1)%pos b)
int_succ_double
  (int_pos_sub (a~1)%pos (pos_succ (b~1)%pos)) =
int_pred_double (int_pos_sub (a~1)%pos (b~1)%pos)
  +
b: Pos
IHb: int_succ_double (int_pos_sub 1%pos (pos_succ b)) =
int_pred_double (int_pos_sub 1%pos b)
int_succ_double
  (int_pos_sub 1%pos (pos_succ (b~1)%pos)) =
int_pred_double (int_pos_sub 1%pos (b~1)%pos) cbn; apply ap.
b: Pos
IHb: int_succ_double (int_pos_sub 1%pos (pos_succ b)) =
int_pred_double (int_pos_sub 1%pos b)
pos_pred_double (pos_pred_double (pos_succ b)) =
(b~0~1)%pos
    by rewrite pos_pred_double_succ.
  +
a: Pos
IHa: forall b : Pos,
int_succ_double (int_pos_sub a (pos_succ b)) =
int_pred_double (int_pos_sub a b)
int_succ_double
  (int_pos_sub (a~0)%pos (pos_succ 1%pos)) =
int_pred_double (int_pos_sub (a~0)%pos 1%pos) destruct a; trivial.
  +
a: Pos
IHa: forall b : Pos,
int_succ_double (int_pos_sub a (pos_succ b)) =
int_pred_double (int_pos_sub a b)
b: Pos
IHb: int_succ_double (int_pos_sub (a~0)%pos (pos_succ b)) =
int_pred_double (int_pos_sub (a~0)%pos b)
int_succ_double
  (int_pos_sub (a~0)%pos (pos_succ (b~0)%pos)) =
int_pred_double (int_pos_sub (a~0)%pos (b~0)%pos) cbn; destruct (int_pos_sub a b); trivial.
  +
a: Pos
IHa: forall b : Pos,
int_succ_double (int_pos_sub a (pos_succ b)) =
int_pred_double (int_pos_sub a b)
b: Pos
IHb: int_succ_double (int_pos_sub (a~0)%pos (pos_succ b)) =
int_pred_double (int_pos_sub (a~0)%pos b)
int_succ_double
  (int_pos_sub (a~0)%pos (pos_succ (b~1)%pos)) =
int_pred_double (int_pos_sub (a~0)%pos (b~1)%pos) cbn.
a: Pos
IHa: forall b : Pos,
int_succ_double (int_pos_sub a (pos_succ b)) =
int_pred_double (int_pos_sub a b)
b: Pos
IHb: int_succ_double (int_pos_sub (a~0)%pos (pos_succ b)) =
int_pred_double (int_pos_sub (a~0)%pos b)
int_succ_double
  (int_double (int_pos_sub a (pos_succ b))) =
int_pred_double (int_pred_double (int_pos_sub a b))
    rewrite <- IHa.
a: Pos
IHa: forall b : Pos,
int_succ_double (int_pos_sub a (pos_succ b)) =
int_pred_double (int_pos_sub a b)
b: Pos
IHb: int_succ_double (int_pos_sub (a~0)%pos (pos_succ b)) =
int_pred_double (int_pos_sub (a~0)%pos b)
int_succ_double
  (int_double (int_pos_sub a (pos_succ b))) =
int_pred_double
  (int_succ_double (int_pos_sub a (pos_succ b)))
    destruct (int_pos_sub a (pos_succ b)); trivial.
  +
a: Pos
IHa: forall b : Pos,
int_succ_double (int_pos_sub a (pos_succ b)) =
int_pred_double (int_pos_sub a b)
int_succ_double
  (int_pos_sub (a~1)%pos (pos_succ 1%pos)) =
int_pred_double (int_pos_sub (a~1)%pos 1%pos) destruct a; trivial.
  +
a: Pos
IHa: forall b : Pos,
int_succ_double (int_pos_sub a (pos_succ b)) =
int_pred_double (int_pos_sub a b)
b: Pos
IHb: int_succ_double (int_pos_sub (a~1)%pos (pos_succ b)) =
int_pred_double (int_pos_sub (a~1)%pos b)
int_succ_double
  (int_pos_sub (a~1)%pos (pos_succ (b~0)%pos)) =
int_pred_double (int_pos_sub (a~1)%pos (b~0)%pos) cbn; destruct (int_pos_sub a b); trivial.
  +
a: Pos
IHa: forall b : Pos,
int_succ_double (int_pos_sub a (pos_succ b)) =
int_pred_double (int_pos_sub a b)
b: Pos
IHb: int_succ_double (int_pos_sub (a~1)%pos (pos_succ b)) =
int_pred_double (int_pos_sub (a~1)%pos b)
int_succ_double
  (int_pos_sub (a~1)%pos (pos_succ (b~1)%pos)) =
int_pred_double (int_pos_sub (a~1)%pos (b~1)%pos) cbn.
a: Pos
IHa: forall b : Pos,
int_succ_double (int_pos_sub a (pos_succ b)) =
int_pred_double (int_pos_sub a b)
b: Pos
IHb: int_succ_double (int_pos_sub (a~1)%pos (pos_succ b)) =
int_pred_double (int_pos_sub (a~1)%pos b)
int_succ_double
  (int_succ_double (int_pos_sub a (pos_succ b))) =
int_pred_double (int_double (int_pos_sub a b))
    rewrite IHa.
a: Pos
IHa: forall b : Pos,
int_succ_double (int_pos_sub a (pos_succ b)) =
int_pred_double (int_pos_sub a b)
b: Pos
IHb: int_succ_double (int_pos_sub (a~1)%pos (pos_succ b)) =
int_pred_double (int_pos_sub (a~1)%pos b)
int_succ_double (int_pred_double (int_pos_sub a b)) =
int_pred_double (int_double (int_pos_sub a b))
    cbn; destruct (int_pos_sub a b); trivial.
Defined.

Lemma int_pred_double_int_pos_sub a b 
  : int_pred_double (int_pos_sub (pos_succ a) b)
    = int_succ_double (int_pos_sub a b).
a, b: Pos
int_pred_double (int_pos_sub (pos_succ a) b) =
int_succ_double (int_pos_sub a b)
Proof.
a, b: Pos
int_pred_double (int_pos_sub (pos_succ a) b) =
int_succ_double (int_pos_sub a b)
  revert a b.
forall a b : Pos,
int_pred_double (int_pos_sub (pos_succ a) b) =
int_succ_double (int_pos_sub a b)
  induction a; induction b; trivial.
b: Pos
IHb: int_pred_double (int_pos_sub (pos_succ 1%pos) b) =
int_succ_double (int_pos_sub 1%pos b)
int_pred_double
  (int_pos_sub (pos_succ 1%pos) (b~0)%pos) =
int_succ_double (int_pos_sub 1%pos (b~0)%pos)
b: Pos
IHb: int_pred_double (int_pos_sub (pos_succ 1%pos) b) =
int_succ_double (int_pos_sub 1%pos b)
int_pred_double
  (int_pos_sub (pos_succ 1%pos) (b~1)%pos) =
int_succ_double (int_pos_sub 1%pos (b~1)%pos)
a: Pos
IHa: forall b : Pos,
int_pred_double (int_pos_sub (pos_succ a) b) =
int_succ_double (int_pos_sub a b)
b: Pos
IHb: int_pred_double (int_pos_sub (pos_succ (a~0)%pos) b) =
int_succ_double (int_pos_sub (a~0)%pos b)
int_pred_double
  (int_pos_sub (pos_succ (a~0)%pos) (b~0)%pos) =
int_succ_double (int_pos_sub (a~0)%pos (b~0)%pos)
a: Pos
IHa: forall b : Pos,
int_pred_double (int_pos_sub (pos_succ a) b) =
int_succ_double (int_pos_sub a b)
b: Pos
IHb: int_pred_double (int_pos_sub (pos_succ (a~0)%pos) b) =
int_succ_double (int_pos_sub (a~0)%pos b)
int_pred_double
  (int_pos_sub (pos_succ (a~0)%pos) (b~1)%pos) =
int_succ_double (int_pos_sub (a~0)%pos (b~1)%pos)
a: Pos
IHa: forall b : Pos,
int_pred_double (int_pos_sub (pos_succ a) b) =
int_succ_double (int_pos_sub a b)
int_pred_double
  (int_pos_sub (pos_succ (a~1)%pos) 1%pos) =
int_succ_double (int_pos_sub (a~1)%pos 1%pos)
a: Pos
IHa: forall b : Pos,
int_pred_double (int_pos_sub (pos_succ a) b) =
int_succ_double (int_pos_sub a b)
b: Pos
IHb: int_pred_double (int_pos_sub (pos_succ (a~1)%pos) b) =
int_succ_double (int_pos_sub (a~1)%pos b)
int_pred_double
  (int_pos_sub (pos_succ (a~1)%pos) (b~0)%pos) =
int_succ_double (int_pos_sub (a~1)%pos (b~0)%pos)
a: Pos
IHa: forall b : Pos,
int_pred_double (int_pos_sub (pos_succ a) b) =
int_succ_double (int_pos_sub a b)
b: Pos
IHb: int_pred_double (int_pos_sub (pos_succ (a~1)%pos) b) =
int_succ_double (int_pos_sub (a~1)%pos b)
int_pred_double
  (int_pos_sub (pos_succ (a~1)%pos) (b~1)%pos) =
int_succ_double (int_pos_sub (a~1)%pos (b~1)%pos)
  +
b: Pos
IHb: int_pred_double (int_pos_sub (pos_succ 1%pos) b) =
int_succ_double (int_pos_sub 1%pos b)
int_pred_double
  (int_pos_sub (pos_succ 1%pos) (b~0)%pos) =
int_succ_double (int_pos_sub 1%pos (b~0)%pos) by destruct b.
  +
b: Pos
IHb: int_pred_double (int_pos_sub (pos_succ 1%pos) b) =
int_succ_double (int_pos_sub 1%pos b)
int_pred_double
  (int_pos_sub (pos_succ 1%pos) (b~1)%pos) =
int_succ_double (int_pos_sub 1%pos (b~1)%pos) by destruct b.
  +
a: Pos
IHa: forall b : Pos,
int_pred_double (int_pos_sub (pos_succ a) b) =
int_succ_double (int_pos_sub a b)
b: Pos
IHb: int_pred_double (int_pos_sub (pos_succ (a~0)%pos) b) =
int_succ_double (int_pos_sub (a~0)%pos b)
int_pred_double
  (int_pos_sub (pos_succ (a~0)%pos) (b~0)%pos) =
int_succ_double (int_pos_sub (a~0)%pos (b~0)%pos) cbn; by destruct (int_pos_sub a b).
  +
a: Pos
IHa: forall b : Pos,
int_pred_double (int_pos_sub (pos_succ a) b) =
int_succ_double (int_pos_sub a b)
b: Pos
IHb: int_pred_double (int_pos_sub (pos_succ (a~0)%pos) b) =
int_succ_double (int_pos_sub (a~0)%pos b)
int_pred_double
  (int_pos_sub (pos_succ (a~0)%pos) (b~1)%pos) =
int_succ_double (int_pos_sub (a~0)%pos (b~1)%pos) cbn; by destruct (int_pos_sub a b).
  +
a: Pos
IHa: forall b : Pos,
int_pred_double (int_pos_sub (pos_succ a) b) =
int_succ_double (int_pos_sub a b)
int_pred_double
  (int_pos_sub (pos_succ (a~1)%pos) 1%pos) =
int_succ_double (int_pos_sub (a~1)%pos 1%pos) cbn; apply ap.
a: Pos
IHa: forall b : Pos,
int_pred_double (int_pos_sub (pos_succ a) b) =
int_succ_double (int_pos_sub a b)
pos_pred_double (pos_pred_double (pos_succ a)) =
(a~0~1)%pos
    by rewrite pos_pred_double_succ.
  +
a: Pos
IHa: forall b : Pos,
int_pred_double (int_pos_sub (pos_succ a) b) =
int_succ_double (int_pos_sub a b)
b: Pos
IHb: int_pred_double (int_pos_sub (pos_succ (a~1)%pos) b) =
int_succ_double (int_pos_sub (a~1)%pos b)
int_pred_double
  (int_pos_sub (pos_succ (a~1)%pos) (b~0)%pos) =
int_succ_double (int_pos_sub (a~1)%pos (b~0)%pos) cbn.
a: Pos
IHa: forall b : Pos,
int_pred_double (int_pos_sub (pos_succ a) b) =
int_succ_double (int_pos_sub a b)
b: Pos
IHb: int_pred_double (int_pos_sub (pos_succ (a~1)%pos) b) =
int_succ_double (int_pos_sub (a~1)%pos b)
int_pred_double
  (int_double (int_pos_sub (pos_succ a) b)) =
int_succ_double (int_succ_double (int_pos_sub a b))
    rewrite <- IHa.
a: Pos
IHa: forall b : Pos,
int_pred_double (int_pos_sub (pos_succ a) b) =
int_succ_double (int_pos_sub a b)
b: Pos
IHb: int_pred_double (int_pos_sub (pos_succ (a~1)%pos) b) =
int_succ_double (int_pos_sub (a~1)%pos b)
int_pred_double
  (int_double (int_pos_sub (pos_succ a) b)) =
int_succ_double
  (int_pred_double (int_pos_sub (pos_succ a) b))
    by destruct (int_pos_sub (pos_succ a) b).
  +
a: Pos
IHa: forall b : Pos,
int_pred_double (int_pos_sub (pos_succ a) b) =
int_succ_double (int_pos_sub a b)
b: Pos
IHb: int_pred_double (int_pos_sub (pos_succ (a~1)%pos) b) =
int_succ_double (int_pos_sub (a~1)%pos b)
int_pred_double
  (int_pos_sub (pos_succ (a~1)%pos) (b~1)%pos) =
int_succ_double (int_pos_sub (a~1)%pos (b~1)%pos) cbn.
a: Pos
IHa: forall b : Pos,
int_pred_double (int_pos_sub (pos_succ a) b) =
int_succ_double (int_pos_sub a b)
b: Pos
IHb: int_pred_double (int_pos_sub (pos_succ (a~1)%pos) b) =
int_succ_double (int_pos_sub (a~1)%pos b)
int_pred_double
  (int_pred_double (int_pos_sub (pos_succ a) b)) =
int_succ_double (int_double (int_pos_sub a b))
    rewrite IHa.
a: Pos
IHa: forall b : Pos,
int_pred_double (int_pos_sub (pos_succ a) b) =
int_succ_double (int_pos_sub a b)
b: Pos
IHb: int_pred_double (int_pos_sub (pos_succ (a~1)%pos) b) =
int_succ_double (int_pos_sub (a~1)%pos b)
int_pred_double (int_succ_double (int_pos_sub a b)) =
int_succ_double (int_double (int_pos_sub a b))
    by destruct (int_pos_sub a b).
Defined.

(** ** Subtractions cancel sucessors. *)
Lemma int_pos_sub_succ_succ a b
  : int_pos_sub (pos_succ a) (pos_succ b) = int_pos_sub a b.
a, b: Pos
int_pos_sub (pos_succ a) (pos_succ b) =
int_pos_sub a b
Proof.
a, b: Pos
int_pos_sub (pos_succ a) (pos_succ b) =
int_pos_sub a b
  rewrite <- 2 pos_add_1_r.
a, b: Pos
int_pos_sub (a + 1)%pos (b + 1)%pos = int_pos_sub a b
  revert a b.
forall a b : Pos,
int_pos_sub (a + 1)%pos (b + 1)%pos = int_pos_sub a b
  induction a; induction b; trivial.
b: Pos
IHb: int_pos_sub (1 + 1)%pos (b + 1)%pos = int_pos_sub 1%pos b
int_pos_sub (1 + 1)%pos (b~0 + 1)%pos =
int_pos_sub 1%pos (b~0)%pos
b: Pos
IHb: int_pos_sub (1 + 1)%pos (b + 1)%pos = int_pos_sub 1%pos b
int_pos_sub (1 + 1)%pos (b~1 + 1)%pos =
int_pos_sub 1%pos (b~1)%pos
a: Pos
IHa: forall b : Pos, int_pos_sub (a + 1)%pos (b + 1)%pos = int_pos_sub a b
int_pos_sub (a~0 + 1)%pos (1 + 1)%pos =
int_pos_sub (a~0)%pos 1%pos
a: Pos
IHa: forall b : Pos, int_pos_sub (a + 1)%pos (b + 1)%pos = int_pos_sub a b
b: Pos
IHb: int_pos_sub (a~0 + 1)%pos (b + 1)%pos = int_pos_sub (a~0)%pos b
int_pos_sub (a~0 + 1)%pos (b~1 + 1)%pos =
int_pos_sub (a~0)%pos (b~1)%pos
a: Pos
IHa: forall b : Pos, int_pos_sub (a + 1)%pos (b + 1)%pos = int_pos_sub a b
int_pos_sub (a~1 + 1)%pos (1 + 1)%pos =
int_pos_sub (a~1)%pos 1%pos
a: Pos
IHa: forall b : Pos, int_pos_sub (a + 1)%pos (b + 1)%pos = int_pos_sub a b
b: Pos
IHb: int_pos_sub (a~1 + 1)%pos (b + 1)%pos = int_pos_sub (a~1)%pos b
int_pos_sub (a~1 + 1)%pos (b~0 + 1)%pos =
int_pos_sub (a~1)%pos (b~0)%pos
a: Pos
IHa: forall b : Pos, int_pos_sub (a + 1)%pos (b + 1)%pos = int_pos_sub a b
b: Pos
IHb: int_pos_sub (a~1 + 1)%pos (b + 1)%pos = int_pos_sub (a~1)%pos b
int_pos_sub (a~1 + 1)%pos (b~1 + 1)%pos =
int_pos_sub (a~1)%pos (b~1)%pos
  1: destruct b; trivial.
b: Pos
IHb: int_pos_sub (1 + 1)%pos (b + 1)%pos = int_pos_sub 1%pos b
int_pos_sub (1 + 1)%pos (b~1 + 1)%pos =
int_pos_sub 1%pos (b~1)%pos
a: Pos
IHa: forall b : Pos, int_pos_sub (a + 1)%pos (b + 1)%pos = int_pos_sub a b
int_pos_sub (a~0 + 1)%pos (1 + 1)%pos =
int_pos_sub (a~0)%pos 1%pos
a: Pos
IHa: forall b : Pos, int_pos_sub (a + 1)%pos (b + 1)%pos = int_pos_sub a b
b: Pos
IHb: int_pos_sub (a~0 + 1)%pos (b + 1)%pos = int_pos_sub (a~0)%pos b
int_pos_sub (a~0 + 1)%pos (b~1 + 1)%pos =
int_pos_sub (a~0)%pos (b~1)%pos
a: Pos
IHa: forall b : Pos, int_pos_sub (a + 1)%pos (b + 1)%pos = int_pos_sub a b
int_pos_sub (a~1 + 1)%pos (1 + 1)%pos =
int_pos_sub (a~1)%pos 1%pos
a: Pos
IHa: forall b : Pos, int_pos_sub (a + 1)%pos (b + 1)%pos = int_pos_sub a b
b: Pos
IHb: int_pos_sub (a~1 + 1)%pos (b + 1)%pos = int_pos_sub (a~1)%pos b
int_pos_sub (a~1 + 1)%pos (b~0 + 1)%pos =
int_pos_sub (a~1)%pos (b~0)%pos
a: Pos
IHa: forall b : Pos, int_pos_sub (a + 1)%pos (b + 1)%pos = int_pos_sub a b
b: Pos
IHb: int_pos_sub (a~1 + 1)%pos (b + 1)%pos = int_pos_sub (a~1)%pos b
int_pos_sub (a~1 + 1)%pos (b~1 + 1)%pos =
int_pos_sub (a~1)%pos (b~1)%pos
  {
b: Pos
IHb: int_pos_sub (1 + 1)%pos (b + 1)%pos = int_pos_sub 1%pos b
int_pos_sub (1 + 1)%pos (b~1 + 1)%pos =
int_pos_sub 1%pos (b~1)%pos destruct b; trivial.
b: Pos
IHb: int_pos_sub (1 + 1)%pos (b~1 + 1)%pos = int_pos_sub 1%pos (b~1)%pos
int_pos_sub (1 + 1)%pos (b~1~1 + 1)%pos =
int_pos_sub 1%pos (b~1~1)%pos
    cbn; apply ap.
b: Pos
IHb: int_pos_sub (1 + 1)%pos (b~1 + 1)%pos = int_pos_sub 1%pos (b~1)%pos
((pos_pred_double (pos_succ b))~0)%pos = (b~1~0)%pos
    by rewrite pos_pred_double_succ. }
a: Pos
IHa: forall b : Pos, int_pos_sub (a + 1)%pos (b + 1)%pos = int_pos_sub a b
int_pos_sub (a~0 + 1)%pos (1 + 1)%pos =
int_pos_sub (a~0)%pos 1%pos
a: Pos
IHa: forall b : Pos, int_pos_sub (a + 1)%pos (b + 1)%pos = int_pos_sub a b
b: Pos
IHb: int_pos_sub (a~0 + 1)%pos (b + 1)%pos = int_pos_sub (a~0)%pos b
int_pos_sub (a~0 + 1)%pos (b~1 + 1)%pos =
int_pos_sub (a~0)%pos (b~1)%pos
a: Pos
IHa: forall b : Pos, int_pos_sub (a + 1)%pos (b + 1)%pos = int_pos_sub a b
int_pos_sub (a~1 + 1)%pos (1 + 1)%pos =
int_pos_sub (a~1)%pos 1%pos
a: Pos
IHa: forall b : Pos, int_pos_sub (a + 1)%pos (b + 1)%pos = int_pos_sub a b
b: Pos
IHb: int_pos_sub (a~1 + 1)%pos (b + 1)%pos = int_pos_sub (a~1)%pos b
int_pos_sub (a~1 + 1)%pos (b~0 + 1)%pos =
int_pos_sub (a~1)%pos (b~0)%pos
a: Pos
IHa: forall b : Pos, int_pos_sub (a + 1)%pos (b + 1)%pos = int_pos_sub a b
b: Pos
IHb: int_pos_sub (a~1 + 1)%pos (b + 1)%pos = int_pos_sub (a~1)%pos b
int_pos_sub (a~1 + 1)%pos (b~1 + 1)%pos =
int_pos_sub (a~1)%pos (b~1)%pos
  1: destruct a; trivial.
a: Pos
IHa: forall b : Pos, int_pos_sub (a + 1)%pos (b + 1)%pos = int_pos_sub a b
b: Pos
IHb: int_pos_sub (a~0 + 1)%pos (b + 1)%pos = int_pos_sub (a~0)%pos b
int_pos_sub (a~0 + 1)%pos (b~1 + 1)%pos =
int_pos_sub (a~0)%pos (b~1)%pos
a: Pos
IHa: forall b : Pos, int_pos_sub (a + 1)%pos (b + 1)%pos = int_pos_sub a b
int_pos_sub (a~1 + 1)%pos (1 + 1)%pos =
int_pos_sub (a~1)%pos 1%pos
a: Pos
IHa: forall b : Pos, int_pos_sub (a + 1)%pos (b + 1)%pos = int_pos_sub a b
b: Pos
IHb: int_pos_sub (a~1 + 1)%pos (b + 1)%pos = int_pos_sub (a~1)%pos b
int_pos_sub (a~1 + 1)%pos (b~0 + 1)%pos =
int_pos_sub (a~1)%pos (b~0)%pos
a: Pos
IHa: forall b : Pos, int_pos_sub (a + 1)%pos (b + 1)%pos = int_pos_sub a b
b: Pos
IHb: int_pos_sub (a~1 + 1)%pos (b + 1)%pos = int_pos_sub (a~1)%pos b
int_pos_sub (a~1 + 1)%pos (b~1 + 1)%pos =
int_pos_sub (a~1)%pos (b~1)%pos
  1: apply int_succ_double_int_pos_sub.
a: Pos
IHa: forall b : Pos, int_pos_sub (a + 1)%pos (b + 1)%pos = int_pos_sub a b
int_pos_sub (a~1 + 1)%pos (1 + 1)%pos =
int_pos_sub (a~1)%pos 1%pos
a: Pos
IHa: forall b : Pos, int_pos_sub (a + 1)%pos (b + 1)%pos = int_pos_sub a b
b: Pos
IHb: int_pos_sub (a~1 + 1)%pos (b + 1)%pos = int_pos_sub (a~1)%pos b
int_pos_sub (a~1 + 1)%pos (b~0 + 1)%pos =
int_pos_sub (a~1)%pos (b~0)%pos
a: Pos
IHa: forall b : Pos, int_pos_sub (a + 1)%pos (b + 1)%pos = int_pos_sub a b
b: Pos
IHb: int_pos_sub (a~1 + 1)%pos (b + 1)%pos = int_pos_sub (a~1)%pos b
int_pos_sub (a~1 + 1)%pos (b~1 + 1)%pos =
int_pos_sub (a~1)%pos (b~1)%pos
  {
a: Pos
IHa: forall b : Pos, int_pos_sub (a + 1)%pos (b + 1)%pos = int_pos_sub a b
int_pos_sub (a~1 + 1)%pos (1 + 1)%pos =
int_pos_sub (a~1)%pos 1%pos destruct a; trivial.
a: Pos
IHa: forall b : Pos,
int_pos_sub (a~1 + 1)%pos (b + 1)%pos = int_pos_sub (a~1)%pos b
int_pos_sub (a~1~1 + 1)%pos (1 + 1)%pos =
int_pos_sub (a~1~1)%pos 1%pos
    cbn; apply ap, ap, pos_pred_double_succ. }
a: Pos
IHa: forall b : Pos, int_pos_sub (a + 1)%pos (b + 1)%pos = int_pos_sub a b
b: Pos
IHb: int_pos_sub (a~1 + 1)%pos (b + 1)%pos = int_pos_sub (a~1)%pos b
int_pos_sub (a~1 + 1)%pos (b~0 + 1)%pos =
int_pos_sub (a~1)%pos (b~0)%pos
a: Pos
IHa: forall b : Pos, int_pos_sub (a + 1)%pos (b + 1)%pos = int_pos_sub a b
b: Pos
IHb: int_pos_sub (a~1 + 1)%pos (b + 1)%pos = int_pos_sub (a~1)%pos b
int_pos_sub (a~1 + 1)%pos (b~1 + 1)%pos =
int_pos_sub (a~1)%pos (b~1)%pos
  1: apply int_pred_double_int_pos_sub.
a: Pos
IHa: forall b : Pos, int_pos_sub (a + 1)%pos (b + 1)%pos = int_pos_sub a b
b: Pos
IHb: int_pos_sub (a~1 + 1)%pos (b + 1)%pos = int_pos_sub (a~1)%pos b
int_pos_sub (a~1 + 1)%pos (b~1 + 1)%pos =
int_pos_sub (a~1)%pos (b~1)%pos
  cbn; apply ap.
a: Pos
IHa: forall b : Pos, int_pos_sub (a + 1)%pos (b + 1)%pos = int_pos_sub a b
b: Pos
IHb: int_pos_sub (a~1 + 1)%pos (b + 1)%pos = int_pos_sub (a~1)%pos b
int_pos_sub (pos_succ a) (pos_succ b) =
int_pos_sub a b
  rewrite <- 2 pos_add_1_r.
a: Pos
IHa: forall b : Pos, int_pos_sub (a + 1)%pos (b + 1)%pos = int_pos_sub a b
b: Pos
IHb: int_pos_sub (a~1 + 1)%pos (b + 1)%pos = int_pos_sub (a~1)%pos b
int_pos_sub (a + 1)%pos (b + 1)%pos = int_pos_sub a b
  apply IHa.
Defined.

(** ** Predecessor of a subtraction is the subtraction of a sucessor. *)
Lemma int_pred_pos_sub_r a b
  : int_pred (int_pos_sub a b) = int_pos_sub a (pos_succ b).
a, b: Pos
int_pred (int_pos_sub a b) =
int_pos_sub a (pos_succ b)
Proof.
a, b: Pos
int_pred (int_pos_sub a b) =
int_pos_sub a (pos_succ b)
  revert a.
b: Pos
forall a : Pos,
int_pred (int_pos_sub a b) =
int_pos_sub a (pos_succ b)
  induction b as [|b bH] using pos_peano_ind.
forall a : Pos,
int_pred (int_pos_sub a 1%pos) =
int_pos_sub a (pos_succ 1%pos)
b: Pos
bH: forall a : Pos,
int_pred (int_pos_sub a b) =
int_pos_sub a (pos_succ b)
forall a : Pos,
int_pred (int_pos_sub a (pos_succ b)) =
int_pos_sub a (pos_succ (pos_succ b))
  1: destruct a; trivial; destruct a; trivial.
b: Pos
bH: forall a : Pos,
int_pred (int_pos_sub a b) =
int_pos_sub a (pos_succ b)
forall a : Pos,
int_pred (int_pos_sub a (pos_succ b)) =
int_pos_sub a (pos_succ (pos_succ b))
  intro a.
b: Pos
bH: forall a : Pos,
int_pred (int_pos_sub a b) =
int_pos_sub a (pos_succ b)
a: Pos
int_pred (int_pos_sub a (pos_succ b)) =
int_pos_sub a (pos_succ (pos_succ b))
  revert b bH.
a: Pos
forall b : Pos,
(forall a : Pos,
 int_pred (int_pos_sub a b) =
 int_pos_sub a (pos_succ b)) ->
int_pred (int_pos_sub a (pos_succ b)) =
int_pos_sub a (pos_succ (pos_succ b))
  induction a as [|a aH] using pos_peano_ind.
forall b : Pos,
(forall a : Pos,
 int_pred (int_pos_sub a b) =
 int_pos_sub a (pos_succ b)) ->
int_pred (int_pos_sub 1%pos (pos_succ b)) =
int_pos_sub 1%pos (pos_succ (pos_succ b))
a: Pos
aH: forall b : Pos,
(forall a : Pos,
 int_pred (int_pos_sub a b) =
 int_pos_sub a (pos_succ b)) ->
int_pred (int_pos_sub a (pos_succ b)) =
int_pos_sub a (pos_succ (pos_succ b))
forall b : Pos,
(forall a : Pos,
 int_pred (int_pos_sub a b) =
 int_pos_sub a (pos_succ b)) ->
int_pred (int_pos_sub (pos_succ a) (pos_succ b)) =
int_pos_sub (pos_succ a) (pos_succ (pos_succ b))
  {
forall b : Pos,
(forall a : Pos,
 int_pred (int_pos_sub a b) =
 int_pos_sub a (pos_succ b)) ->
int_pred (int_pos_sub 1%pos (pos_succ b)) =
int_pos_sub 1%pos (pos_succ (pos_succ b)) intros b bH.
b: Pos
bH: forall a : Pos,
int_pred (int_pos_sub a b) =
int_pos_sub a (pos_succ b)
int_pred (int_pos_sub 1%pos (pos_succ b)) =
int_pos_sub 1%pos (pos_succ (pos_succ b))
    rewrite <- bH.
b: Pos
bH: forall a : Pos,
int_pred (int_pos_sub a b) =
int_pos_sub a (pos_succ b)
int_pred (int_pred (int_pos_sub 1%pos b)) =
int_pos_sub 1%pos (pos_succ (pos_succ b))
    destruct b; trivial.
b: Pos
bH: forall a : Pos,
int_pred (int_pos_sub a (b~0)%pos) =
int_pos_sub a (pos_succ (b~0)%pos)
int_pred (int_pred (int_pos_sub 1%pos (b~0)%pos)) =
int_pos_sub 1%pos (pos_succ (pos_succ (b~0)%pos))
    cbn; apply ap.
b: Pos
bH: forall a : Pos,
int_pred (int_pos_sub a (b~0)%pos) =
int_pos_sub a (pos_succ (b~0)%pos)
(pos_pred_double b + 1 + 1)%pos =
pos_pred_double (pos_succ b)
    rewrite 2 pos_add_1_r.
b: Pos
bH: forall a : Pos,
int_pred (int_pos_sub a (b~0)%pos) =
int_pos_sub a (pos_succ (b~0)%pos)
pos_succ (pos_succ (pos_pred_double b)) =
pos_pred_double (pos_succ b)
    rewrite pos_succ_pred_double.
b: Pos
bH: forall a : Pos,
int_pred (int_pos_sub a (b~0)%pos) =
int_pos_sub a (pos_succ (b~0)%pos)
pos_succ (b~0)%pos = pos_pred_double (pos_succ b)
    rewrite pos_pred_double_succ.
b: Pos
bH: forall a : Pos,
int_pred (int_pos_sub a (b~0)%pos) =
int_pos_sub a (pos_succ (b~0)%pos)
pos_succ (b~0)%pos = (b~1)%pos
    trivial. }
a: Pos
aH: forall b : Pos,
(forall a : Pos,
 int_pred (int_pos_sub a b) =
 int_pos_sub a (pos_succ b)) ->
int_pred (int_pos_sub a (pos_succ b)) =
int_pos_sub a (pos_succ (pos_succ b))
forall b : Pos,
(forall a : Pos,
 int_pred (int_pos_sub a b) =
 int_pos_sub a (pos_succ b)) ->
int_pred (int_pos_sub (pos_succ a) (pos_succ b)) =
int_pos_sub (pos_succ a) (pos_succ (pos_succ b))
  intros b bH.
a: Pos
aH: forall b : Pos,
(forall a : Pos,
 int_pred (int_pos_sub a b) =
 int_pos_sub a (pos_succ b)) ->
int_pred (int_pos_sub a (pos_succ b)) =
int_pos_sub a (pos_succ (pos_succ b))
b: Pos
bH: forall a : Pos,
int_pred (int_pos_sub a b) =
int_pos_sub a (pos_succ b)
int_pred (int_pos_sub (pos_succ a) (pos_succ b)) =
int_pos_sub (pos_succ a) (pos_succ (pos_succ b))
  rewrite 2 int_pos_sub_succ_succ.
a: Pos
aH: forall b : Pos,
(forall a : Pos,
 int_pred (int_pos_sub a b) =
 int_pos_sub a (pos_succ b)) ->
int_pred (int_pos_sub a (pos_succ b)) =
int_pos_sub a (pos_succ (pos_succ b))
b: Pos
bH: forall a : Pos,
int_pred (int_pos_sub a b) =
int_pos_sub a (pos_succ b)
int_pred (int_pos_sub a b) =
int_pos_sub a (pos_succ b)
  apply bH.
Defined.

(** ** Negation of the predecessor is an involution. *)
Lemma int_negation_pred_negation_red x
  : - int_pred (- int_pred x) = x.
x: Int
- int_pred (- int_pred x) = x
Proof.
x: Int
- int_pred (- int_pred x) = x
  destruct x as [x| |x]; trivial;
  destruct x; trivial; cbn; apply ap.
x: Pos
pos_pred_double (pos_succ x) = (x~1)%pos
x: Pos
(pos_pred_double x + 1)%pos = (x~0)%pos
  1: apply pos_pred_double_succ.
x: Pos
(pos_pred_double x + 1)%pos = (x~0)%pos
  rewrite pos_add_1_r.
x: Pos
pos_succ (pos_pred_double x) = (x~0)%pos
  apply pos_succ_pred_double.
Defined.

(** ** Predecessor of a sum is the sum with a predecessor *)
Lemma int_pred_add_r a b
  : int_pred (a + b) = a + int_pred b.
a, b: Int
int_pred (a + b) = a + int_pred b
Proof.
a, b: Int
int_pred (a + b) = a + int_pred b
  revert a b.
forall a b : Int, int_pred (a + b) = a + int_pred b
  intros [a| |a] [b| |b]; trivial.
a, b: Pos
int_pred (neg a + neg b) = neg a + int_pred (neg b)
a, b: Pos
int_pred (neg a + pos b) = neg a + int_pred (pos b)
a, b: Pos
int_pred (pos a + neg b) = pos a + int_pred (neg b)
a, b: Pos
int_pred (pos a + pos b) = pos a + int_pred (pos b)
  +
a, b: Pos
int_pred (neg a + neg b) = neg a + int_pred (neg b) cbn; apply ap.
a, b: Pos
(a + b + 1)%pos = (a + (b + 1))%pos
    by rewrite pos_add_assoc.
  +
a, b: Pos
int_pred (neg a + pos b) = neg a + int_pred (pos b) revert a.
b: Pos
forall a : Pos,
int_pred (neg a + pos b) = neg a + int_pred (pos b)
    induction b as [|b bH] using pos_peano_ind.
forall a : Pos,
int_pred (neg a + 1) = neg a + int_pred 1
b: Pos
bH: forall a : Pos,
int_pred (neg a + pos b) =
neg a + int_pred (pos b)
forall a : Pos,
int_pred (neg a + pos (pos_succ b)) =
neg a + int_pred (pos (pos_succ b))
    -
forall a : Pos,
int_pred (neg a + 1) = neg a + int_pred 1 intro a; exact (int_pred_succ (neg a)).
    -
b: Pos
bH: forall a : Pos,
int_pred (neg a + pos b) =
neg a + int_pred (pos b)
forall a : Pos,
int_pred (neg a + pos (pos_succ b)) =
neg a + int_pred (pos (pos_succ b)) intro a.
b: Pos
bH: forall a : Pos,
int_pred (neg a + pos b) =
neg a + int_pred (pos b)
a: Pos
int_pred (neg a + pos (pos_succ b)) =
neg a + int_pred (pos (pos_succ b))
      rewrite <- pos_add_1_r.
b: Pos
bH: forall a : Pos,
int_pred (neg a + pos b) =
neg a + int_pred (pos b)
a: Pos
int_pred (neg a + pos (b + 1%pos)) =
neg a + int_pred (pos (b + 1%pos))
      rewrite (int_pred_succ (pos b)).
b: Pos
bH: forall a : Pos,
int_pred (neg a + pos b) =
neg a + int_pred (pos b)
a: Pos
int_pred (neg a + pos (b + 1%pos)) = neg a + pos b
      rewrite int_add_comm.
b: Pos
bH: forall a : Pos,
int_pred (neg a + pos b) =
neg a + int_pred (pos b)
a: Pos
int_pred (pos (b + 1%pos) + neg a) = neg a + pos b
      cbn.
b: Pos
bH: forall a : Pos,
int_pred (neg a + pos b) =
neg a + int_pred (pos b)
a: Pos
int_pred (int_pos_sub (b + 1)%pos a) = int_pos_sub b a
      rewrite pos_add_1_r.
b: Pos
bH: forall a : Pos,
int_pred (neg a + pos b) =
neg a + int_pred (pos b)
a: Pos
int_pred (int_pos_sub (pos_succ b) a) =
int_pos_sub b a
      rewrite <- int_pos_sub_negation.
b: Pos
bH: forall a : Pos,
int_pred (neg a + pos b) =
neg a + int_pred (pos b)
a: Pos
int_pred (- int_pos_sub a (pos_succ b)) =
int_pos_sub b a
      rewrite <- int_pred_pos_sub_r.
b: Pos
bH: forall a : Pos,
int_pred (neg a + pos b) =
neg a + int_pred (pos b)
a: Pos
int_pred (- int_pred (int_pos_sub a b)) =
int_pos_sub b a
      apply int_negation_inj.
b: Pos
bH: forall a : Pos,
int_pred (neg a + pos b) =
neg a + int_pred (pos b)
a: Pos
- int_pred (- int_pred (int_pos_sub a b)) =
- int_pos_sub b a
      rewrite int_pos_sub_negation.
b: Pos
bH: forall a : Pos,
int_pred (neg a + pos b) =
neg a + int_pred (pos b)
a: Pos
- int_pred (- int_pred (int_pos_sub a b)) =
int_pos_sub a b
      apply int_negation_pred_negation_red.
  +
a, b: Pos
int_pred (pos a + neg b) = pos a + int_pred (neg b) cbn.
a, b: Pos
int_pred (int_pos_sub a b) = int_pos_sub a (b + 1)%pos
    rewrite pos_add_1_r.
a, b: Pos
int_pred (int_pos_sub a b) =
int_pos_sub a (pos_succ b)
    apply int_pred_pos_sub_r.
  +
a, b: Pos
int_pred (pos a + pos b) = pos a + int_pred (pos b) revert a.
b: Pos
forall a : Pos,
int_pred (pos a + pos b) = pos a + int_pred (pos b)
    induction b as [|b bH] using pos_peano_ind.
forall a : Pos,
int_pred (pos a + 1) = pos a + int_pred 1
b: Pos
bH: forall a : Pos,
int_pred (pos a + pos b) =
pos a + int_pred (pos b)
forall a : Pos,
int_pred (pos a + pos (pos_succ b)) =
pos a + int_pred (pos (pos_succ b))
    -
forall a : Pos,
int_pred (pos a + 1) = pos a + int_pred 1 intro a; exact (int_pred_succ (pos a)).
    -
b: Pos
bH: forall a : Pos,
int_pred (pos a + pos b) =
pos a + int_pred (pos b)
forall a : Pos,
int_pred (pos a + pos (pos_succ b)) =
pos a + int_pred (pos (pos_succ b)) intro a.
b: Pos
bH: forall a : Pos,
int_pred (pos a + pos b) =
pos a + int_pred (pos b)
a: Pos
int_pred (pos a + pos (pos_succ b)) =
pos a + int_pred (pos (pos_succ b))
      rewrite <- pos_add_1_r.
b: Pos
bH: forall a : Pos,
int_pred (pos a + pos b) =
pos a + int_pred (pos b)
a: Pos
int_pred (pos a + pos (b + 1%pos)) =
pos a + int_pred (pos (b + 1%pos))
      rewrite (int_pred_succ (pos b)).
b: Pos
bH: forall a : Pos,
int_pred (pos a + pos b) =
pos a + int_pred (pos b)
a: Pos
int_pred (pos a + pos (b + 1%pos)) = pos a + pos b
      cbn; rewrite pos_add_assoc.
b: Pos
bH: forall a : Pos,
int_pred (pos a + pos b) =
pos a + int_pred (pos b)
a: Pos
match (a + b + 1)%pos with
| 1%pos => 0
| (p~0)%pos => pos (pos_pred_double p)
| (p~1)%pos => pos p~0
end = pos (a + b)
      change (int_pred (int_succ (pos (a + b)%pos)) = pos a + pos b).
b: Pos
bH: forall a : Pos,
int_pred (pos a + pos b) =
pos a + int_pred (pos b)
a: Pos
int_pred (int_succ (pos (a + b))) = pos a + pos b
      apply int_pred_succ.
Defined.

(** ** Subtraction from a sum is the sum of a subtraction *)
Lemma int_pos_sub_add (a b c : Pos)
  : int_pos_sub (a + b)%pos c = pos a + int_pos_sub b c.
a, b, c: Pos
int_pos_sub (a + b)%pos c = pos a + int_pos_sub b c
Proof.
a, b, c: Pos
int_pos_sub (a + b)%pos c = pos a + int_pos_sub b c
  revert c b a.
forall c b a : Pos,
int_pos_sub (a + b)%pos c = pos a + int_pos_sub b c
  induction c as [|c ch] using pos_peano_ind.
forall b a : Pos,
int_pos_sub (a + b)%pos 1%pos =
pos a + int_pos_sub b 1%pos
c: Pos
ch: forall b a : Pos,
int_pos_sub (a + b)%pos c =
pos a + int_pos_sub b c
forall b a : Pos,
int_pos_sub (a + b)%pos (pos_succ c) =
pos a + int_pos_sub b (pos_succ c)
  {
forall b a : Pos,
int_pos_sub (a + b)%pos 1%pos =
pos a + int_pos_sub b 1%pos intros b a.
b, a: Pos
int_pos_sub (a + b)%pos 1%pos =
pos a + int_pos_sub b 1%pos
    change (int_pred (pos a + pos b) = pos a + (int_pred (pos b))).
b, a: Pos
int_pred (pos a + pos b) = pos a + int_pred (pos b)
    apply int_pred_add_r. }
c: Pos
ch: forall b a : Pos,
int_pos_sub (a + b)%pos c =
pos a + int_pos_sub b c
forall b a : Pos,
int_pos_sub (a + b)%pos (pos_succ c) =
pos a + int_pos_sub b (pos_succ c)
  intros b a.
c: Pos
ch: forall b a : Pos,
int_pos_sub (a + b)%pos c =
pos a + int_pos_sub b c
b, a: Pos
int_pos_sub (a + b)%pos (pos_succ c) =
pos a + int_pos_sub b (pos_succ c)
  rewrite <- int_pred_pos_sub_r.
c: Pos
ch: forall b a : Pos,
int_pos_sub (a + b)%pos c =
pos a + int_pos_sub b c
b, a: Pos
int_pred (int_pos_sub (a + b)%pos c) =
pos a + int_pos_sub b (pos_succ c)
  rewrite ch.
c: Pos
ch: forall b a : Pos,
int_pos_sub (a + b)%pos c =
pos a + int_pos_sub b c
b, a: Pos
int_pred (pos a + int_pos_sub b c) =
pos a + int_pos_sub b (pos_succ c)
  rewrite <- int_pred_pos_sub_r.
c: Pos
ch: forall b a : Pos,
int_pos_sub (a + b)%pos c =
pos a + int_pos_sub b c
b, a: Pos
int_pred (pos a + int_pos_sub b c) =
pos a + int_pred (int_pos_sub b c)
  apply int_pred_add_r.
Defined.

(** An auxillary lemma used to prove associativity. *)
Lemma int_add_assoc_pos p n m : pos p + (n + m) = pos p + n + m.
p: Pos
n, m: Int
pos p + (n + m) = pos p + n + m
Proof.
p: Pos
n, m: Int
pos p + (n + m) = pos p + n + m
  destruct n as [n| |n], m as [m| |m]; trivial.
p, n, m: Pos
pos p + (neg n + neg m) = pos p + neg n + neg m
p, n: Pos
pos p + (neg n + 0) = pos p + neg n + 0
p, n, m: Pos
pos p + (neg n + pos m) = pos p + neg n + pos m
p, n, m: Pos
pos p + (pos n + neg m) = pos p + pos n + neg m
p, n, m: Pos
pos p + (pos n + pos m) = pos p + pos n + pos m
  -
p, n, m: Pos
pos p + (neg n + neg m) = pos p + neg n + neg m cbn; apply int_negation_inj.
p, n, m: Pos
- int_pos_sub p (n + m)%pos =
- (int_pos_sub p n + neg m)
    rewrite !int_negation_add_distr, !int_pos_sub_negation.
p, n, m: Pos
int_pos_sub (n + m)%pos p = int_pos_sub n p + - neg m
    rewrite int_add_comm, pos_add_comm.
p, n, m: Pos
int_pos_sub (m + n)%pos p = - neg m + int_pos_sub n p
    apply int_pos_sub_add.
  -
p, n: Pos
pos p + (neg n + 0) = pos p + neg n + 0 symmetry.
p, n: Pos
pos p + neg n + 0 = pos p + (neg n + 0)
    apply int_add_0_r.
  -
p, n, m: Pos
pos p + (neg n + pos m) = pos p + neg n + pos m by rewrite <- int_pos_sub_add, int_add_comm,
      <- int_pos_sub_add, pos_add_comm.
  -
p, n, m: Pos
pos p + (pos n + neg m) = pos p + pos n + neg m symmetry.
p, n, m: Pos
pos p + pos n + neg m = pos p + (pos n + neg m)
    apply int_pos_sub_add.
  -
p, n, m: Pos
pos p + (pos n + pos m) = pos p + pos n + pos m cbn; apply ap, pos_add_assoc.
Defined.

(** ** Associativity of addition *)
Lemma int_add_assoc n m p : n + (m + p) = n + m + p.
n, m, p: Int
n + (m + p) = n + m + p
Proof.
n, m, p: Int
n + (m + p) = n + m + p
  destruct n.
p0: Pos
m, p: Int
neg p0 + (m + p) = neg p0 + m + p
m, p: Int
0 + (m + p) = 0 + m + p
p0: Pos
m, p: Int
pos p0 + (m + p) = pos p0 + m + p
  -
p0: Pos
m, p: Int
neg p0 + (m + p) = neg p0 + m + p apply int_negation_inj.
p0: Pos
m, p: Int
- (neg p0 + (m + p)) = - (neg p0 + m + p)
    rewrite !int_negation_add_distr.
p0: Pos
m, p: Int
- neg p0 + (- m + - p) = - neg p0 + - m + - p
    apply int_add_assoc_pos.
  -
m, p: Int
0 + (m + p) = 0 + m + p trivial.
  -
p0: Pos
m, p: Int
pos p0 + (m + p) = pos p0 + m + p apply int_add_assoc_pos.
Defined.

(** ** Relationship between [int_succ], [int_pred] and addition. *)
Lemma int_add_succ_l a b : int_succ a + b = int_succ (a + b).
a, b: Int
int_succ a + b = int_succ (a + b)
Proof.
a, b: Int
int_succ a + b = int_succ (a + b)
  rewrite <- int_add_assoc, (int_add_comm 1 b).
a, b: Int
a + (b + 1) = int_succ (a + b)
  apply int_add_assoc.
Defined.

Lemma int_add_succ_r a b : a + int_succ b = int_succ (a + b).
a, b: Int
a + int_succ b = int_succ (a + b)
Proof.
a, b: Int
a + int_succ b = int_succ (a + b)
  apply int_add_assoc.
Defined.

Lemma int_add_pred_l a b : int_pred a + b = int_pred (a + b).
a, b: Int
int_pred a + b = int_pred (a + b)
Proof.
a, b: Int
int_pred a + b = int_pred (a + b)
  rewrite <- int_add_assoc, (int_add_comm (-1) b).
a, b: Int
a + (b + -1) = int_pred (a + b)
  apply int_add_assoc.
Defined.

Lemma int_add_pred_r a b : a + int_pred b = int_pred (a + b).
a, b: Int
a + int_pred b = int_pred (a + b)
Proof.
a, b: Int
a + int_pred b = int_pred (a + b)
  apply int_add_assoc.
Defined.

(** ** Commutativity of multiplication *)
Lemma int_mul_comm n m : n * m = m * n.
n, m: Int
n * m = m * n
Proof.
n, m: Int
n * m = m * n
  destruct n, m; cbn; try reflexivity;
  apply ap; apply pos_mul_comm.
Defined.

(** Distributivity of multiplication over addition *)

Lemma int_pos_sub_mul_pos n m p
  : int_pos_sub n m * pos p = int_pos_sub (n * p)%pos (m * p)%pos.
n, m, p: Pos
int_pos_sub n m * pos p =
int_pos_sub (n * p)%pos (m * p)%pos
Proof.
n, m, p: Pos
int_pos_sub n m * pos p =
int_pos_sub (n * p)%pos (m * p)%pos
  rewrite int_mul_comm.
n, m, p: Pos
pos p * int_pos_sub n m =
int_pos_sub (n * p)%pos (m * p)%pos
  rewrite 2 (pos_mul_comm _ p).
n, m, p: Pos
pos p * int_pos_sub n m =
int_pos_sub (p * n)%pos (p * m)%pos
  induction p.
n, m: Pos
1 * int_pos_sub n m =
int_pos_sub (1 * n)%pos (1 * m)%pos
n, m, p: Pos
IHp: pos p * int_pos_sub n m = int_pos_sub (p * n)%pos (p * m)%pos
pos p~0 * int_pos_sub n m =
int_pos_sub (p~0 * n)%pos (p~0 * m)%pos
n, m, p: Pos
IHp: pos p * int_pos_sub n m = int_pos_sub (p * n)%pos (p * m)%pos
pos p~1 * int_pos_sub n m =
int_pos_sub (p~1 * n)%pos (p~1 * m)%pos
  {
n, m: Pos
1 * int_pos_sub n m =
int_pos_sub (1 * n)%pos (1 * m)%pos rewrite 2 pos_mul_1_l.
n, m: Pos
1 * int_pos_sub n m = int_pos_sub n m
    apply int_mul_1_l. }
n, m, p: Pos
IHp: pos p * int_pos_sub n m = int_pos_sub (p * n)%pos (p * m)%pos
pos p~0 * int_pos_sub n m =
int_pos_sub (p~0 * n)%pos (p~0 * m)%pos
n, m, p: Pos
IHp: pos p * int_pos_sub n m = int_pos_sub (p * n)%pos (p * m)%pos
pos p~1 * int_pos_sub n m =
int_pos_sub (p~1 * n)%pos (p~1 * m)%pos
  {
n, m, p: Pos
IHp: pos p * int_pos_sub n m = int_pos_sub (p * n)%pos (p * m)%pos
pos p~0 * int_pos_sub n m =
int_pos_sub (p~0 * n)%pos (p~0 * m)%pos cbn.
n, m, p: Pos
IHp: pos p * int_pos_sub n m = int_pos_sub (p * n)%pos (p * m)%pos
match int_pos_sub n m with
| neg y' => neg ((p * y')~0)%pos
| 0 => 0
| pos y' => pos (p * y')%pos~0
end = int_double (int_pos_sub (p * n)%pos (p * m)%pos)
    rewrite <- IHp.
n, m, p: Pos
IHp: pos p * int_pos_sub n m = int_pos_sub (p * n)%pos (p * m)%pos
match int_pos_sub n m with
| neg y' => neg ((p * y')~0)%pos
| 0 => 0
| pos y' => pos (p * y')%pos~0
end = int_double (pos p * int_pos_sub n m)
    set (int_pos_sub n m) as k.
n, m, p: Pos
IHp: pos p * int_pos_sub n m = int_pos_sub (p * n)%pos (p * m)%pos
k:= int_pos_sub n m: Int
match k with
| neg y' => neg ((p * y')~0)%pos
| 0 => 0
| pos y' => pos (p * y')%pos~0
end = int_double (pos p * k)
    by destruct k. }
n, m, p: Pos
IHp: pos p * int_pos_sub n m = int_pos_sub (p * n)%pos (p * m)%pos
pos p~1 * int_pos_sub n m =
int_pos_sub (p~1 * n)%pos (p~1 * m)%pos
  cbn.
n, m, p: Pos
IHp: pos p * int_pos_sub n m = int_pos_sub (p * n)%pos (p * m)%pos
match int_pos_sub n m with
| neg y' => neg (y' + (p * y')~0)%pos
| 0 => 0
| pos y' => pos (y' + ((p * y')~0)%pos)
end =
int_pos_sub (n + (p * n)~0)%pos (m + (p * m)~0)%pos
  rewrite int_pos_sub_add.
n, m, p: Pos
IHp: pos p * int_pos_sub n m = int_pos_sub (p * n)%pos (p * m)%pos
match int_pos_sub n m with
| neg y' => neg (y' + (p * y')~0)%pos
| 0 => 0
| pos y' => pos (y' + ((p * y')~0)%pos)
end =
pos n +
int_pos_sub ((p * n)~0)%pos (m + (p * m)~0)%pos
  rewrite <- (int_pos_sub_negation _ (x0 _)).
n, m, p: Pos
IHp: pos p * int_pos_sub n m = int_pos_sub (p * n)%pos (p * m)%pos
match int_pos_sub n m with
| neg y' => neg (y' + (p * y')~0)%pos
| 0 => 0
| pos y' => pos (y' + ((p * y')~0)%pos)
end =
pos n +
- int_pos_sub (m + (p * m)~0)%pos ((p * n)~0)%pos
  rewrite int_pos_sub_add.
n, m, p: Pos
IHp: pos p * int_pos_sub n m = int_pos_sub (p * n)%pos (p * m)%pos
match int_pos_sub n m with
| neg y' => neg (y' + (p * y')~0)%pos
| 0 => 0
| pos y' => pos (y' + ((p * y')~0)%pos)
end =
pos n +
-
(pos m + int_pos_sub ((p * m)~0)%pos ((p * n)~0)%pos)
  rewrite int_negation_add_distr.
n, m, p: Pos
IHp: pos p * int_pos_sub n m = int_pos_sub (p * n)%pos (p * m)%pos
match int_pos_sub n m with
| neg y' => neg (y' + (p * y')~0)%pos
| 0 => 0
| pos y' => pos (y' + ((p * y')~0)%pos)
end =
pos n +
(- pos m +
 - int_pos_sub ((p * m)~0)%pos ((p * n)~0)%pos)
  rewrite int_pos_sub_negation.
n, m, p: Pos
IHp: pos p * int_pos_sub n m = int_pos_sub (p * n)%pos (p * m)%pos
match int_pos_sub n m with
| neg y' => neg (y' + (p * y')~0)%pos
| 0 => 0
| pos y' => pos (y' + ((p * y')~0)%pos)
end =
pos n +
(- pos m + int_pos_sub ((p * n)~0)%pos ((p * m)~0)%pos)
  rewrite int_add_assoc.
n, m, p: Pos
IHp: pos p * int_pos_sub n m = int_pos_sub (p * n)%pos (p * m)%pos
match int_pos_sub n m with
| neg y' => neg (y' + (p * y')~0)%pos
| 0 => 0
| pos y' => pos (y' + ((p * y')~0)%pos)
end =
pos n + - pos m +
int_pos_sub ((p * n)~0)%pos ((p * m)~0)%pos
  cbn.
n, m, p: Pos
IHp: pos p * int_pos_sub n m = int_pos_sub (p * n)%pos (p * m)%pos
match int_pos_sub n m with
| neg y' => neg (y' + (p * y')~0)%pos
| 0 => 0
| pos y' => pos (y' + ((p * y')~0)%pos)
end =
int_pos_sub n m +
int_double (int_pos_sub (p * n)%pos (p * m)%pos)
  rewrite <- IHp.
n, m, p: Pos
IHp: pos p * int_pos_sub n m = int_pos_sub (p * n)%pos (p * m)%pos
match int_pos_sub n m with
| neg y' => neg (y' + (p * y')~0)%pos
| 0 => 0
| pos y' => pos (y' + ((p * y')~0)%pos)
end =
int_pos_sub n m + int_double (pos p * int_pos_sub n m)
  set (int_pos_sub n m) as k.
n, m, p: Pos
IHp: pos p * int_pos_sub n m = int_pos_sub (p * n)%pos (p * m)%pos
k:= int_pos_sub n m: Int
match k with
| neg y' => neg (y' + (p * y')~0)%pos
| 0 => 0
| pos y' => pos (y' + ((p * y')~0)%pos)
end = k + int_double (pos p * k)
  by destruct k.
Defined.

Lemma int_pos_sub_mul_neg n m p
  : int_pos_sub m n  * neg p = int_pos_sub (n * p)%pos (m * p)%pos.
n, m, p: Pos
int_pos_sub m n * neg p =
int_pos_sub (n * p)%pos (m * p)%pos
Proof.
n, m, p: Pos
int_pos_sub m n * neg p =
int_pos_sub (n * p)%pos (m * p)%pos
  rewrite int_mul_comm.
n, m, p: Pos
neg p * int_pos_sub m n =
int_pos_sub (n * p)%pos (m * p)%pos
  rewrite 2 (pos_mul_comm _ p).
n, m, p: Pos
neg p * int_pos_sub m n =
int_pos_sub (p * n)%pos (p * m)%pos
  induction p.
n, m: Pos
-1 * int_pos_sub m n =
int_pos_sub (1 * n)%pos (1 * m)%pos
n, m, p: Pos
IHp: neg p * int_pos_sub m n = int_pos_sub (p * n)%pos (p * m)%pos
neg (p~0)%pos * int_pos_sub m n =
int_pos_sub (p~0 * n)%pos (p~0 * m)%pos
n, m, p: Pos
IHp: neg p * int_pos_sub m n = int_pos_sub (p * n)%pos (p * m)%pos
neg (p~1)%pos * int_pos_sub m n =
int_pos_sub (p~1 * n)%pos (p~1 * m)%pos
  {
n, m: Pos
-1 * int_pos_sub m n =
int_pos_sub (1 * n)%pos (1 * m)%pos rewrite 2 pos_mul_1_l.
n, m: Pos
-1 * int_pos_sub m n = int_pos_sub n m
    rewrite <- int_pos_sub_negation.
n, m: Pos
-1 * - int_pos_sub n m = int_pos_sub n m
    by destruct (int_pos_sub n m). }
n, m, p: Pos
IHp: neg p * int_pos_sub m n = int_pos_sub (p * n)%pos (p * m)%pos
neg (p~0)%pos * int_pos_sub m n =
int_pos_sub (p~0 * n)%pos (p~0 * m)%pos
n, m, p: Pos
IHp: neg p * int_pos_sub m n = int_pos_sub (p * n)%pos (p * m)%pos
neg (p~1)%pos * int_pos_sub m n =
int_pos_sub (p~1 * n)%pos (p~1 * m)%pos
  {
n, m, p: Pos
IHp: neg p * int_pos_sub m n = int_pos_sub (p * n)%pos (p * m)%pos
neg (p~0)%pos * int_pos_sub m n =
int_pos_sub (p~0 * n)%pos (p~0 * m)%pos cbn.
n, m, p: Pos
IHp: neg p * int_pos_sub m n = int_pos_sub (p * n)%pos (p * m)%pos
match int_pos_sub m n with
| neg y' => pos (p * y')%pos~0
| 0 => 0
| pos y' => neg ((p * y')~0)%pos
end = int_double (int_pos_sub (p * n)%pos (p * m)%pos)
    rewrite <- IHp.
n, m, p: Pos
IHp: neg p * int_pos_sub m n = int_pos_sub (p * n)%pos (p * m)%pos
match int_pos_sub m n with
| neg y' => pos (p * y')%pos~0
| 0 => 0
| pos y' => neg ((p * y')~0)%pos
end = int_double (neg p * int_pos_sub m n)
    rewrite <- int_pos_sub_negation.
n, m, p: Pos
IHp: neg p * int_pos_sub m n = int_pos_sub (p * n)%pos (p * m)%pos
match - int_pos_sub n m with
| neg y' => pos (p * y')%pos~0
| 0 => 0
| pos y' => neg ((p * y')~0)%pos
end = int_double (neg p * - int_pos_sub n m)
    set (int_pos_sub n m) as k.
n, m, p: Pos
IHp: neg p * int_pos_sub m n = int_pos_sub (p * n)%pos (p * m)%pos
k:= int_pos_sub n m: Int
match - k with
| neg y' => pos (p * y')%pos~0
| 0 => 0
| pos y' => neg ((p * y')~0)%pos
end = int_double (neg p * - k)
    by destruct k. }
n, m, p: Pos
IHp: neg p * int_pos_sub m n = int_pos_sub (p * n)%pos (p * m)%pos
neg (p~1)%pos * int_pos_sub m n =
int_pos_sub (p~1 * n)%pos (p~1 * m)%pos
  cbn.
n, m, p: Pos
IHp: neg p * int_pos_sub m n = int_pos_sub (p * n)%pos (p * m)%pos
match int_pos_sub m n with
| neg y' => pos (y' + ((p * y')~0)%pos)
| 0 => 0
| pos y' => neg (y' + (p * y')~0)%pos
end =
int_pos_sub (n + (p * n)~0)%pos (m + (p * m)~0)%pos
  rewrite int_pos_sub_add.
n, m, p: Pos
IHp: neg p * int_pos_sub m n = int_pos_sub (p * n)%pos (p * m)%pos
match int_pos_sub m n with
| neg y' => pos (y' + ((p * y')~0)%pos)
| 0 => 0
| pos y' => neg (y' + (p * y')~0)%pos
end =
pos n +
int_pos_sub ((p * n)~0)%pos (m + (p * m)~0)%pos
  rewrite <- (int_pos_sub_negation _ (x0 _)).
n, m, p: Pos
IHp: neg p * int_pos_sub m n = int_pos_sub (p * n)%pos (p * m)%pos
match int_pos_sub m n with
| neg y' => pos (y' + ((p * y')~0)%pos)
| 0 => 0
| pos y' => neg (y' + (p * y')~0)%pos
end =
pos n +
- int_pos_sub (m + (p * m)~0)%pos ((p * n)~0)%pos
  rewrite int_pos_sub_add.
n, m, p: Pos
IHp: neg p * int_pos_sub m n = int_pos_sub (p * n)%pos (p * m)%pos
match int_pos_sub m n with
| neg y' => pos (y' + ((p * y')~0)%pos)
| 0 => 0
| pos y' => neg (y' + (p * y')~0)%pos
end =
pos n +
-
(pos m + int_pos_sub ((p * m)~0)%pos ((p * n)~0)%pos)
  rewrite int_negation_add_distr.
n, m, p: Pos
IHp: neg p * int_pos_sub m n = int_pos_sub (p * n)%pos (p * m)%pos
match int_pos_sub m n with
| neg y' => pos (y' + ((p * y')~0)%pos)
| 0 => 0
| pos y' => neg (y' + (p * y')~0)%pos
end =
pos n +
(- pos m +
 - int_pos_sub ((p * m)~0)%pos ((p * n)~0)%pos)
  rewrite int_pos_sub_negation.
n, m, p: Pos
IHp: neg p * int_pos_sub m n = int_pos_sub (p * n)%pos (p * m)%pos
match int_pos_sub m n with
| neg y' => pos (y' + ((p * y')~0)%pos)
| 0 => 0
| pos y' => neg (y' + (p * y')~0)%pos
end =
pos n +
(- pos m + int_pos_sub ((p * n)~0)%pos ((p * m)~0)%pos)
  rewrite int_add_assoc.
n, m, p: Pos
IHp: neg p * int_pos_sub m n = int_pos_sub (p * n)%pos (p * m)%pos
match int_pos_sub m n with
| neg y' => pos (y' + ((p * y')~0)%pos)
| 0 => 0
| pos y' => neg (y' + (p * y')~0)%pos
end =
pos n + - pos m +
int_pos_sub ((p * n)~0)%pos ((p * m)~0)%pos
  cbn.
n, m, p: Pos
IHp: neg p * int_pos_sub m n = int_pos_sub (p * n)%pos (p * m)%pos
match int_pos_sub m n with
| neg y' => pos (y' + ((p * y')~0)%pos)
| 0 => 0
| pos y' => neg (y' + (p * y')~0)%pos
end =
int_pos_sub n m +
int_double (int_pos_sub (p * n)%pos (p * m)%pos)
  rewrite <- IHp.
n, m, p: Pos
IHp: neg p * int_pos_sub m n = int_pos_sub (p * n)%pos (p * m)%pos
match int_pos_sub m n with
| neg y' => pos (y' + ((p * y')~0)%pos)
| 0 => 0
| pos y' => neg (y' + (p * y')~0)%pos
end =
int_pos_sub n m + int_double (neg p * int_pos_sub m n)
  rewrite <- (int_pos_sub_negation m).
n, m, p: Pos
IHp: neg p * int_pos_sub m n = int_pos_sub (p * n)%pos (p * m)%pos
match int_pos_sub m n with
| neg y' => pos (y' + ((p * y')~0)%pos)
| 0 => 0
| pos y' => neg (y' + (p * y')~0)%pos
end =
- int_pos_sub m n +
int_double (neg p * int_pos_sub m n)
  set (int_pos_sub m n) as k.
n, m, p: Pos
IHp: neg p * int_pos_sub m n = int_pos_sub (p * n)%pos (p * m)%pos
k:= int_pos_sub m n: Int
match k with
| neg y' => pos (y' + ((p * y')~0)%pos)
| 0 => 0
| pos y' => neg (y' + (p * y')~0)%pos
end = - k + int_double (neg p * k)
  by destruct k.
Defined.

Lemma int_mul_add_distr_r n m p : (n + m) * p = n * p + m * p.
n, m, p: Int
(n + m) * p = n * p + m * p
Proof.
n, m, p: Int
(n + m) * p = n * p + m * p
  induction p; destruct n, m; cbn; trivial; try f_ap;
  try apply pos_mul_add_distr_r;
  try apply int_pos_sub_mul_neg;
  try apply int_pos_sub_mul_pos;
  apply int_mul_0_r.
Defined.

Lemma int_mul_add_distr_l n m p : n * (m + p) = n * m + n * p.
n, m, p: Int
n * (m + p) = n * m + n * p
Proof.
n, m, p: Int
n * (m + p) = n * m + n * p
  rewrite 3 (int_mul_comm n); apply int_mul_add_distr_r.
Defined.

Lemma int_mul_assoc n m p : n * (m * p) = n * m * p.
n, m, p: Int
n * (m * p) = n * m * p
Proof.
n, m, p: Int
n * (m * p) = n * m * p
  destruct n, m, p; cbn; trivial; f_ap; apply pos_mul_assoc.
Defined.