From HoTT Require Import Basics.From HoTT Require Import Basics.
Require Import Spaces.Pos.
Require Import Spaces.BinInt.Core.

Local Set Universe Minimization ToSet.

Local Open Scope binint_scope.

(** ** Addition is commutative *)

Lemma binint_add_comm n m : n + m = m + n.
n, m: BinInt
n + m = m + n
Proof.
n, m: BinInt
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 binint_add_0_l n : 0 + n = n
  := 1.

Lemma binint_add_0_r n : n + 0 = n.
n: BinInt
n + 0 = n
Proof.
n: BinInt
n + 0 = n
  by destruct n.
Defined.

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

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

Lemma binint_mul_0_r n : n * 0 = 0.
n: BinInt
n * 0 = 0
Proof.
n: BinInt
n * 0 = 0
  by destruct n.
Defined.

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

Lemma binint_mul_1_l n : 1 * n = n.
n: BinInt
1 * n = n
Proof.
n: BinInt
1 * n = n
  by destruct n.
Defined.

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

(** ** Inverse laws *)

Lemma binint_pos_sub_diag n : binint_pos_sub n n = 0.
n: Pos
binint_pos_sub n n = 0
Proof.
n: Pos
binint_pos_sub n n = 0
  induction n; trivial; cbn.
n: Pos
IHn: binint_pos_sub n n = 0
binint_double (binint_pos_sub n n) = 0
n: Pos
IHn: binint_pos_sub n n = 0
binint_double (binint_pos_sub n n) = 0
  all: exact (ap binint_double IHn).
Defined.

Lemma binint_add_negation_l n : (-n) + n = 0.
n: BinInt
- n + n = 0
Proof.
n: BinInt
- n + n = 0
  destruct n; trivial; cbn; apply binint_pos_sub_diag.
Defined.

Lemma binint_add_negation_r n : n + (-n) = 0.
n: BinInt
n + - n = 0
Proof.
n: BinInt
n + - n = 0
  destruct n; trivial; cbn; apply binint_pos_sub_diag.
Defined.

(** ** Permutation of [neg] and [pos_succ] *)
Lemma binint_neg_pos_succ p : neg (pos_succ p) = binint_pred (neg p).
p: Pos
neg (pos_succ p) = binint_pred (neg p)
Proof.
p: Pos
neg (pos_succ p) = binint_pred (neg p)
  by destruct p.
Defined.

(** ** Permutation of [pos] and [pos_succ] *)
Lemma binint_pos_pos_succ p : pos (pos_succ p) = binint_succ (pos p).
p: Pos
pos (pos_succ p) = binint_succ (pos p)
Proof.
p: Pos
pos (pos_succ p) = binint_succ (pos p)
  by destruct p.
Defined.

(** ** Negation of a doubled positive integer *)
Lemma binint_negation_double a : - (binint_double a) = binint_double (- a).
a: BinInt
- binint_double a = binint_double (- a)
Proof.
a: BinInt
- binint_double a = binint_double (- a)
  by destruct a.
Defined.

(** Negation of the predecessor of a doubled positive integer. *)
Lemma binint_negation_pred_double a
  : - (binint_pred_double a) = binint_succ_double (- a).
a: BinInt
- binint_pred_double a = binint_succ_double (- a)
Proof.
a: BinInt
- binint_pred_double a = binint_succ_double (- a)
  by destruct a.
Defined.

(** Negation of the doubling of the successor of an positive. *)
Lemma binint_negation_succ_double a
  : - (binint_succ_double a) = binint_pred_double (- a).
a: BinInt
- binint_succ_double a = binint_pred_double (- a)
Proof.
a: BinInt
- binint_succ_double a = binint_pred_double (- a)
  by destruct a.
Defined.

(** Negation of subtraction of positive integers *)
Lemma binint_pos_sub_negation a b
  : - (binint_pos_sub a b) = binint_pos_sub b a.
a, b: Pos
- binint_pos_sub a b = binint_pos_sub b a
Proof.
a, b: Pos
- binint_pos_sub a b = binint_pos_sub b a
  revert a b.
forall a b : Pos, - binint_pos_sub a b = binint_pos_sub b a
  induction a as [|a ah|a ah];
  destruct b;
  cbn; trivial.
a: Pos
ah: forall b0 : Pos, - binint_pos_sub a b0 = binint_pos_sub b0 a
b: Pos
- binint_double (binint_pos_sub a b) = binint_double (binint_pos_sub b a)
a: Pos
ah: forall b0 : Pos, - binint_pos_sub a b0 = binint_pos_sub b0 a
b: Pos
- binint_pred_double (binint_pos_sub a b) =
binint_succ_double (binint_pos_sub b a)
a: Pos
ah: forall b0 : Pos, - binint_pos_sub a b0 = binint_pos_sub b0 a
b: Pos
- binint_succ_double (binint_pos_sub a b) =
binint_pred_double (binint_pos_sub b a)
a: Pos
ah: forall b0 : Pos, - binint_pos_sub a b0 = binint_pos_sub b0 a
b: Pos
- binint_double (binint_pos_sub a b) = binint_double (binint_pos_sub b a)
  all: rewrite ?binint_negation_double,
    ?binint_negation_succ_double,
    ?binint_negation_pred_double.
a: Pos
ah: forall b0 : Pos, - binint_pos_sub a b0 = binint_pos_sub b0 a
b: Pos
binint_double (- binint_pos_sub a b) = binint_double (binint_pos_sub b a)
a: Pos
ah: forall b0 : Pos, - binint_pos_sub a b0 = binint_pos_sub b0 a
b: Pos
binint_succ_double (- binint_pos_sub a b) =
binint_succ_double (binint_pos_sub b a)
a: Pos
ah: forall b0 : Pos, - binint_pos_sub a b0 = binint_pos_sub b0 a
b: Pos
binint_pred_double (- binint_pos_sub a b) =
binint_pred_double (binint_pos_sub b a)
a: Pos
ah: forall b0 : Pos, - binint_pos_sub a b0 = binint_pos_sub b0 a
b: Pos
binint_double (- binint_pos_sub a b) = binint_double (binint_pos_sub b a)
  all: apply ap, ah.
Defined.

(** ** [binint_succ] is a retract of [binint_pred] *)
Definition binint_succ_pred : binint_succ o binint_pred == idmap.
binint_succ o binint_pred == idmap
Proof.
binint_succ o binint_pred == idmap
  intros [n | | n]; [|trivial|].
n: Pos
binint_succ (binint_pred (neg n)) = neg n
n: Pos
binint_succ (binint_pred (pos n)) = pos n
  all: destruct n; trivial.
n: Pos
binint_succ (binint_pred (neg n~1%pos)) = neg n~1%pos
n: Pos
binint_succ (binint_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.

(** ** [binint_pred] is a retract of [binint_succ] *)
Definition binint_pred_succ : binint_pred o binint_succ == idmap.
binint_pred o binint_succ == idmap
Proof.
binint_pred o binint_succ == idmap
  intros [n | | n]; [|trivial|].
n: Pos
binint_pred (binint_succ (neg n)) = neg n
n: Pos
binint_pred (binint_succ (pos n)) = pos n
  all: destruct n; trivial.
n: Pos
binint_pred (binint_succ (neg n~0%pos)) = neg n~0%pos
n: Pos
binint_pred (binint_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 auto-equivalence. *)
Instance isequiv_binint_succ : IsEquiv binint_succ | 0
  := isequiv_adjointify binint_succ _ binint_succ_pred binint_pred_succ.

Definition equiv_binint_succ : BinInt <~> BinInt
  := Build_Equiv _ _ _ isequiv_binint_succ.

(** ** Negation distributes over addition *)
Lemma binint_negation_add_distr n m : - (n + m) = - n + - m.
n, m: BinInt
- (n + m) = - n + - m
Proof.
n, m: BinInt
- (n + m) = - n + - m
 destruct n, m; simpl; trivial using binint_pos_sub_negation.
Defined.

(** ** Negation is injective *)
Lemma binint_negation_inj n m : -n = -m -> n = m.
n, m: BinInt
- n = - m -> n = m
Proof.
n, m: BinInt
- 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 successor gives the positive integer. *)
Lemma binint_pos_sub_succ_l a
  : binint_pos_sub (pos_succ a) 1%pos = pos a.
a: Pos
binint_pos_sub (pos_succ a) 1%pos = pos a
Proof.
a: Pos
binint_pos_sub (pos_succ a) 1%pos = pos a
  destruct a; trivial.
a: Pos
binint_pos_sub (pos_succ a~1%pos) 1%pos = pos a~1
  cbn; apply ap, pos_pred_double_succ.
Defined.

(** ** Subtracting a successor from 1 gives minus the integer. *)
Lemma binint_pos_sub_succ_r a
  : binint_pos_sub 1%pos (pos_succ a) = neg a.
a: Pos
binint_pos_sub 1%pos (pos_succ a) = neg a
Proof.
a: Pos
binint_pos_sub 1%pos (pos_succ a) = neg a
  destruct a; trivial.
a: Pos
binint_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 binint_succ_double_binint_pos_sub a b
  : binint_succ_double (binint_pos_sub a (pos_succ b))
    = binint_pred_double (binint_pos_sub a b).
a, b: Pos
binint_succ_double (binint_pos_sub a (pos_succ b)) =
binint_pred_double (binint_pos_sub a b)
Proof.
a, b: Pos
binint_succ_double (binint_pos_sub a (pos_succ b)) =
binint_pred_double (binint_pos_sub a b)
  revert a b.
forall a b : Pos,
binint_succ_double (binint_pos_sub a (pos_succ b)) =
binint_pred_double (binint_pos_sub a b)
  induction a; induction b; trivial.
b: Pos
IHb: binint_succ_double (binint_pos_sub 1%pos (pos_succ b)) =
binint_pred_double (binint_pos_sub 1%pos b)
binint_succ_double (binint_pos_sub 1%pos (pos_succ b~1%pos)) =
binint_pred_double (binint_pos_sub 1%pos b~1%pos)
a: Pos
IHa: forall b : Pos,
binint_succ_double (binint_pos_sub a (pos_succ b)) =
binint_pred_double (binint_pos_sub a b)
binint_succ_double (binint_pos_sub a~0%pos (pos_succ 1%pos)) =
binint_pred_double (binint_pos_sub a~0%pos 1%pos)
a: Pos
IHa: forall b0 : Pos,
binint_succ_double (binint_pos_sub a (pos_succ b0)) =
binint_pred_double (binint_pos_sub a b0)
b: Pos
IHb: binint_succ_double (binint_pos_sub a~0%pos (pos_succ b)) =
binint_pred_double (binint_pos_sub a~0%pos b)
binint_succ_double (binint_pos_sub a~0%pos (pos_succ b~0%pos)) =
binint_pred_double (binint_pos_sub a~0%pos b~0%pos)
a: Pos
IHa: forall b0 : Pos,
binint_succ_double (binint_pos_sub a (pos_succ b0)) =
binint_pred_double (binint_pos_sub a b0)
b: Pos
IHb: binint_succ_double (binint_pos_sub a~0%pos (pos_succ b)) =
binint_pred_double (binint_pos_sub a~0%pos b)
binint_succ_double (binint_pos_sub a~0%pos (pos_succ b~1%pos)) =
binint_pred_double (binint_pos_sub a~0%pos b~1%pos)
a: Pos
IHa: forall b : Pos,
binint_succ_double (binint_pos_sub a (pos_succ b)) =
binint_pred_double (binint_pos_sub a b)
binint_succ_double (binint_pos_sub a~1%pos (pos_succ 1%pos)) =
binint_pred_double (binint_pos_sub a~1%pos 1%pos)
a: Pos
IHa: forall b0 : Pos,
binint_succ_double (binint_pos_sub a (pos_succ b0)) =
binint_pred_double (binint_pos_sub a b0)
b: Pos
IHb: binint_succ_double (binint_pos_sub a~1%pos (pos_succ b)) =
binint_pred_double (binint_pos_sub a~1%pos b)
binint_succ_double (binint_pos_sub a~1%pos (pos_succ b~0%pos)) =
binint_pred_double (binint_pos_sub a~1%pos b~0%pos)
a: Pos
IHa: forall b0 : Pos,
binint_succ_double (binint_pos_sub a (pos_succ b0)) =
binint_pred_double (binint_pos_sub a b0)
b: Pos
IHb: binint_succ_double (binint_pos_sub a~1%pos (pos_succ b)) =
binint_pred_double (binint_pos_sub a~1%pos b)
binint_succ_double (binint_pos_sub a~1%pos (pos_succ b~1%pos)) =
binint_pred_double (binint_pos_sub a~1%pos b~1%pos)
  +
b: Pos
IHb: binint_succ_double (binint_pos_sub 1%pos (pos_succ b)) =
binint_pred_double (binint_pos_sub 1%pos b)
binint_succ_double (binint_pos_sub 1%pos (pos_succ b~1%pos)) =
binint_pred_double (binint_pos_sub 1%pos b~1%pos) cbn; apply ap.
b: Pos
IHb: binint_succ_double (binint_pos_sub 1%pos (pos_succ b)) =
binint_pred_double (binint_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,
binint_succ_double (binint_pos_sub a (pos_succ b)) =
binint_pred_double (binint_pos_sub a b)
binint_succ_double (binint_pos_sub a~0%pos (pos_succ 1%pos)) =
binint_pred_double (binint_pos_sub a~0%pos 1%pos) destruct a; trivial.
  +
a: Pos
IHa: forall b0 : Pos,
binint_succ_double (binint_pos_sub a (pos_succ b0)) =
binint_pred_double (binint_pos_sub a b0)
b: Pos
IHb: binint_succ_double (binint_pos_sub a~0%pos (pos_succ b)) =
binint_pred_double (binint_pos_sub a~0%pos b)
binint_succ_double (binint_pos_sub a~0%pos (pos_succ b~0%pos)) =
binint_pred_double (binint_pos_sub a~0%pos b~0%pos) cbn; destruct (binint_pos_sub a b); trivial.
  +
a: Pos
IHa: forall b0 : Pos,
binint_succ_double (binint_pos_sub a (pos_succ b0)) =
binint_pred_double (binint_pos_sub a b0)
b: Pos
IHb: binint_succ_double (binint_pos_sub a~0%pos (pos_succ b)) =
binint_pred_double (binint_pos_sub a~0%pos b)
binint_succ_double (binint_pos_sub a~0%pos (pos_succ b~1%pos)) =
binint_pred_double (binint_pos_sub a~0%pos b~1%pos) cbn.
a: Pos
IHa: forall b0 : Pos,
binint_succ_double (binint_pos_sub a (pos_succ b0)) =
binint_pred_double (binint_pos_sub a b0)
b: Pos
IHb: binint_succ_double (binint_pos_sub a~0%pos (pos_succ b)) =
binint_pred_double (binint_pos_sub a~0%pos b)
binint_succ_double (binint_double (binint_pos_sub a (pos_succ b))) =
binint_pred_double (binint_pred_double (binint_pos_sub a b))
    rewrite <- IHa.
a: Pos
IHa: forall b0 : Pos,
binint_succ_double (binint_pos_sub a (pos_succ b0)) =
binint_pred_double (binint_pos_sub a b0)
b: Pos
IHb: binint_succ_double (binint_pos_sub a~0%pos (pos_succ b)) =
binint_pred_double (binint_pos_sub a~0%pos b)
binint_succ_double (binint_double (binint_pos_sub a (pos_succ b))) =
binint_pred_double (binint_succ_double (binint_pos_sub a (pos_succ b)))
    destruct (binint_pos_sub a (pos_succ b)); trivial.
  +
a: Pos
IHa: forall b : Pos,
binint_succ_double (binint_pos_sub a (pos_succ b)) =
binint_pred_double (binint_pos_sub a b)
binint_succ_double (binint_pos_sub a~1%pos (pos_succ 1%pos)) =
binint_pred_double (binint_pos_sub a~1%pos 1%pos) destruct a; trivial.
  +
a: Pos
IHa: forall b0 : Pos,
binint_succ_double (binint_pos_sub a (pos_succ b0)) =
binint_pred_double (binint_pos_sub a b0)
b: Pos
IHb: binint_succ_double (binint_pos_sub a~1%pos (pos_succ b)) =
binint_pred_double (binint_pos_sub a~1%pos b)
binint_succ_double (binint_pos_sub a~1%pos (pos_succ b~0%pos)) =
binint_pred_double (binint_pos_sub a~1%pos b~0%pos) cbn; destruct (binint_pos_sub a b); trivial.
  +
a: Pos
IHa: forall b0 : Pos,
binint_succ_double (binint_pos_sub a (pos_succ b0)) =
binint_pred_double (binint_pos_sub a b0)
b: Pos
IHb: binint_succ_double (binint_pos_sub a~1%pos (pos_succ b)) =
binint_pred_double (binint_pos_sub a~1%pos b)
binint_succ_double (binint_pos_sub a~1%pos (pos_succ b~1%pos)) =
binint_pred_double (binint_pos_sub a~1%pos b~1%pos) cbn.
a: Pos
IHa: forall b0 : Pos,
binint_succ_double (binint_pos_sub a (pos_succ b0)) =
binint_pred_double (binint_pos_sub a b0)
b: Pos
IHb: binint_succ_double (binint_pos_sub a~1%pos (pos_succ b)) =
binint_pred_double (binint_pos_sub a~1%pos b)
binint_succ_double (binint_succ_double (binint_pos_sub a (pos_succ b))) =
binint_pred_double (binint_double (binint_pos_sub a b))
    rewrite IHa.
a: Pos
IHa: forall b0 : Pos,
binint_succ_double (binint_pos_sub a (pos_succ b0)) =
binint_pred_double (binint_pos_sub a b0)
b: Pos
IHb: binint_succ_double (binint_pos_sub a~1%pos (pos_succ b)) =
binint_pred_double (binint_pos_sub a~1%pos b)
binint_succ_double (binint_pred_double (binint_pos_sub a b)) =
binint_pred_double (binint_double (binint_pos_sub a b))
    cbn; destruct (binint_pos_sub a b); trivial.
Defined.

Lemma binint_pred_double_binint_pos_sub a b 
  : binint_pred_double (binint_pos_sub (pos_succ a) b)
    = binint_succ_double (binint_pos_sub a b).
a, b: Pos
binint_pred_double (binint_pos_sub (pos_succ a) b) =
binint_succ_double (binint_pos_sub a b)
Proof.
a, b: Pos
binint_pred_double (binint_pos_sub (pos_succ a) b) =
binint_succ_double (binint_pos_sub a b)
  revert a b.
forall a b : Pos,
binint_pred_double (binint_pos_sub (pos_succ a) b) =
binint_succ_double (binint_pos_sub a b)
  induction a; induction b; trivial.
b: Pos
IHb: binint_pred_double (binint_pos_sub (pos_succ 1%pos) b) =
binint_succ_double (binint_pos_sub 1%pos b)
binint_pred_double (binint_pos_sub (pos_succ 1%pos) b~0%pos) =
binint_succ_double (binint_pos_sub 1%pos b~0%pos)
b: Pos
IHb: binint_pred_double (binint_pos_sub (pos_succ 1%pos) b) =
binint_succ_double (binint_pos_sub 1%pos b)
binint_pred_double (binint_pos_sub (pos_succ 1%pos) b~1%pos) =
binint_succ_double (binint_pos_sub 1%pos b~1%pos)
a: Pos
IHa: forall b0 : Pos,
binint_pred_double (binint_pos_sub (pos_succ a) b0) =
binint_succ_double (binint_pos_sub a b0)
b: Pos
IHb: binint_pred_double (binint_pos_sub (pos_succ a~0%pos) b) =
binint_succ_double (binint_pos_sub a~0%pos b)
binint_pred_double (binint_pos_sub (pos_succ a~0%pos) b~0%pos) =
binint_succ_double (binint_pos_sub a~0%pos b~0%pos)
a: Pos
IHa: forall b0 : Pos,
binint_pred_double (binint_pos_sub (pos_succ a) b0) =
binint_succ_double (binint_pos_sub a b0)
b: Pos
IHb: binint_pred_double (binint_pos_sub (pos_succ a~0%pos) b) =
binint_succ_double (binint_pos_sub a~0%pos b)
binint_pred_double (binint_pos_sub (pos_succ a~0%pos) b~1%pos) =
binint_succ_double (binint_pos_sub a~0%pos b~1%pos)
a: Pos
IHa: forall b : Pos,
binint_pred_double (binint_pos_sub (pos_succ a) b) =
binint_succ_double (binint_pos_sub a b)
binint_pred_double (binint_pos_sub (pos_succ a~1%pos) 1%pos) =
binint_succ_double (binint_pos_sub a~1%pos 1%pos)
a: Pos
IHa: forall b0 : Pos,
binint_pred_double (binint_pos_sub (pos_succ a) b0) =
binint_succ_double (binint_pos_sub a b0)
b: Pos
IHb: binint_pred_double (binint_pos_sub (pos_succ a~1%pos) b) =
binint_succ_double (binint_pos_sub a~1%pos b)
binint_pred_double (binint_pos_sub (pos_succ a~1%pos) b~0%pos) =
binint_succ_double (binint_pos_sub a~1%pos b~0%pos)
a: Pos
IHa: forall b0 : Pos,
binint_pred_double (binint_pos_sub (pos_succ a) b0) =
binint_succ_double (binint_pos_sub a b0)
b: Pos
IHb: binint_pred_double (binint_pos_sub (pos_succ a~1%pos) b) =
binint_succ_double (binint_pos_sub a~1%pos b)
binint_pred_double (binint_pos_sub (pos_succ a~1%pos) b~1%pos) =
binint_succ_double (binint_pos_sub a~1%pos b~1%pos)
  +
b: Pos
IHb: binint_pred_double (binint_pos_sub (pos_succ 1%pos) b) =
binint_succ_double (binint_pos_sub 1%pos b)
binint_pred_double (binint_pos_sub (pos_succ 1%pos) b~0%pos) =
binint_succ_double (binint_pos_sub 1%pos b~0%pos) by destruct b.
  +
b: Pos
IHb: binint_pred_double (binint_pos_sub (pos_succ 1%pos) b) =
binint_succ_double (binint_pos_sub 1%pos b)
binint_pred_double (binint_pos_sub (pos_succ 1%pos) b~1%pos) =
binint_succ_double (binint_pos_sub 1%pos b~1%pos) by destruct b.
  +
a: Pos
IHa: forall b0 : Pos,
binint_pred_double (binint_pos_sub (pos_succ a) b0) =
binint_succ_double (binint_pos_sub a b0)
b: Pos
IHb: binint_pred_double (binint_pos_sub (pos_succ a~0%pos) b) =
binint_succ_double (binint_pos_sub a~0%pos b)
binint_pred_double (binint_pos_sub (pos_succ a~0%pos) b~0%pos) =
binint_succ_double (binint_pos_sub a~0%pos b~0%pos) cbn; by destruct (binint_pos_sub a b).
  +
a: Pos
IHa: forall b0 : Pos,
binint_pred_double (binint_pos_sub (pos_succ a) b0) =
binint_succ_double (binint_pos_sub a b0)
b: Pos
IHb: binint_pred_double (binint_pos_sub (pos_succ a~0%pos) b) =
binint_succ_double (binint_pos_sub a~0%pos b)
binint_pred_double (binint_pos_sub (pos_succ a~0%pos) b~1%pos) =
binint_succ_double (binint_pos_sub a~0%pos b~1%pos) cbn; by destruct (binint_pos_sub a b).
  +
a: Pos
IHa: forall b : Pos,
binint_pred_double (binint_pos_sub (pos_succ a) b) =
binint_succ_double (binint_pos_sub a b)
binint_pred_double (binint_pos_sub (pos_succ a~1%pos) 1%pos) =
binint_succ_double (binint_pos_sub a~1%pos 1%pos) cbn; apply ap.
a: Pos
IHa: forall b : Pos,
binint_pred_double (binint_pos_sub (pos_succ a) b) =
binint_succ_double (binint_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 b0 : Pos,
binint_pred_double (binint_pos_sub (pos_succ a) b0) =
binint_succ_double (binint_pos_sub a b0)
b: Pos
IHb: binint_pred_double (binint_pos_sub (pos_succ a~1%pos) b) =
binint_succ_double (binint_pos_sub a~1%pos b)
binint_pred_double (binint_pos_sub (pos_succ a~1%pos) b~0%pos) =
binint_succ_double (binint_pos_sub a~1%pos b~0%pos) cbn.
a: Pos
IHa: forall b0 : Pos,
binint_pred_double (binint_pos_sub (pos_succ a) b0) =
binint_succ_double (binint_pos_sub a b0)
b: Pos
IHb: binint_pred_double (binint_pos_sub (pos_succ a~1%pos) b) =
binint_succ_double (binint_pos_sub a~1%pos b)
binint_pred_double (binint_double (binint_pos_sub (pos_succ a) b)) =
binint_succ_double (binint_succ_double (binint_pos_sub a b))
    rewrite <- IHa.
a: Pos
IHa: forall b0 : Pos,
binint_pred_double (binint_pos_sub (pos_succ a) b0) =
binint_succ_double (binint_pos_sub a b0)
b: Pos
IHb: binint_pred_double (binint_pos_sub (pos_succ a~1%pos) b) =
binint_succ_double (binint_pos_sub a~1%pos b)
binint_pred_double (binint_double (binint_pos_sub (pos_succ a) b)) =
binint_succ_double (binint_pred_double (binint_pos_sub (pos_succ a) b))
    by destruct (binint_pos_sub (pos_succ a) b).
  +
a: Pos
IHa: forall b0 : Pos,
binint_pred_double (binint_pos_sub (pos_succ a) b0) =
binint_succ_double (binint_pos_sub a b0)
b: Pos
IHb: binint_pred_double (binint_pos_sub (pos_succ a~1%pos) b) =
binint_succ_double (binint_pos_sub a~1%pos b)
binint_pred_double (binint_pos_sub (pos_succ a~1%pos) b~1%pos) =
binint_succ_double (binint_pos_sub a~1%pos b~1%pos) cbn.
a: Pos
IHa: forall b0 : Pos,
binint_pred_double (binint_pos_sub (pos_succ a) b0) =
binint_succ_double (binint_pos_sub a b0)
b: Pos
IHb: binint_pred_double (binint_pos_sub (pos_succ a~1%pos) b) =
binint_succ_double (binint_pos_sub a~1%pos b)
binint_pred_double (binint_pred_double (binint_pos_sub (pos_succ a) b)) =
binint_succ_double (binint_double (binint_pos_sub a b))
    rewrite IHa.
a: Pos
IHa: forall b0 : Pos,
binint_pred_double (binint_pos_sub (pos_succ a) b0) =
binint_succ_double (binint_pos_sub a b0)
b: Pos
IHb: binint_pred_double (binint_pos_sub (pos_succ a~1%pos) b) =
binint_succ_double (binint_pos_sub a~1%pos b)
binint_pred_double (binint_succ_double (binint_pos_sub a b)) =
binint_succ_double (binint_double (binint_pos_sub a b))
    by destruct (binint_pos_sub a b).
Defined.

(** ** Subtractions cancel successors. *)
Lemma binint_pos_sub_succ_succ a b
  : binint_pos_sub (pos_succ a) (pos_succ b) = binint_pos_sub a b.
a, b: Pos
binint_pos_sub (pos_succ a) (pos_succ b) = binint_pos_sub a b
Proof.
a, b: Pos
binint_pos_sub (pos_succ a) (pos_succ b) = binint_pos_sub a b
  rewrite <- 2 pos_add_1_r.
a, b: Pos
binint_pos_sub (a + 1)%pos (b + 1)%pos = binint_pos_sub a b
  revert a b.
forall a b : Pos, binint_pos_sub (a + 1)%pos (b + 1)%pos = binint_pos_sub a b
  induction a; induction b; trivial.
b: Pos
IHb: binint_pos_sub (1 + 1)%pos (b + 1)%pos = binint_pos_sub 1%pos b
binint_pos_sub (1 + 1)%pos (b~0 + 1)%pos = binint_pos_sub 1%pos b~0%pos
b: Pos
IHb: binint_pos_sub (1 + 1)%pos (b + 1)%pos = binint_pos_sub 1%pos b
binint_pos_sub (1 + 1)%pos (b~1 + 1)%pos = binint_pos_sub 1%pos b~1%pos
a: Pos
IHa: forall b : Pos, binint_pos_sub (a + 1)%pos (b + 1)%pos = binint_pos_sub a b
binint_pos_sub (a~0 + 1)%pos (1 + 1)%pos = binint_pos_sub a~0%pos 1%pos
a: Pos
IHa: forall b0 : Pos,
binint_pos_sub (a + 1)%pos (b0 + 1)%pos = binint_pos_sub a b0
b: Pos
IHb: binint_pos_sub (a~0 + 1)%pos (b + 1)%pos = binint_pos_sub a~0%pos b
binint_pos_sub (a~0 + 1)%pos (b~1 + 1)%pos = binint_pos_sub a~0%pos b~1%pos
a: Pos
IHa: forall b : Pos, binint_pos_sub (a + 1)%pos (b + 1)%pos = binint_pos_sub a b
binint_pos_sub (a~1 + 1)%pos (1 + 1)%pos = binint_pos_sub a~1%pos 1%pos
a: Pos
IHa: forall b0 : Pos,
binint_pos_sub (a + 1)%pos (b0 + 1)%pos = binint_pos_sub a b0
b: Pos
IHb: binint_pos_sub (a~1 + 1)%pos (b + 1)%pos = binint_pos_sub a~1%pos b
binint_pos_sub (a~1 + 1)%pos (b~0 + 1)%pos = binint_pos_sub a~1%pos b~0%pos
a: Pos
IHa: forall b0 : Pos,
binint_pos_sub (a + 1)%pos (b0 + 1)%pos = binint_pos_sub a b0
b: Pos
IHb: binint_pos_sub (a~1 + 1)%pos (b + 1)%pos = binint_pos_sub a~1%pos b
binint_pos_sub (a~1 + 1)%pos (b~1 + 1)%pos = binint_pos_sub a~1%pos b~1%pos
  1: destruct b; trivial.
b: Pos
IHb: binint_pos_sub (1 + 1)%pos (b + 1)%pos = binint_pos_sub 1%pos b
binint_pos_sub (1 + 1)%pos (b~1 + 1)%pos = binint_pos_sub 1%pos b~1%pos
a: Pos
IHa: forall b : Pos, binint_pos_sub (a + 1)%pos (b + 1)%pos = binint_pos_sub a b
binint_pos_sub (a~0 + 1)%pos (1 + 1)%pos = binint_pos_sub a~0%pos 1%pos
a: Pos
IHa: forall b0 : Pos,
binint_pos_sub (a + 1)%pos (b0 + 1)%pos = binint_pos_sub a b0
b: Pos
IHb: binint_pos_sub (a~0 + 1)%pos (b + 1)%pos = binint_pos_sub a~0%pos b
binint_pos_sub (a~0 + 1)%pos (b~1 + 1)%pos = binint_pos_sub a~0%pos b~1%pos
a: Pos
IHa: forall b : Pos, binint_pos_sub (a + 1)%pos (b + 1)%pos = binint_pos_sub a b
binint_pos_sub (a~1 + 1)%pos (1 + 1)%pos = binint_pos_sub a~1%pos 1%pos
a: Pos
IHa: forall b0 : Pos,
binint_pos_sub (a + 1)%pos (b0 + 1)%pos = binint_pos_sub a b0
b: Pos
IHb: binint_pos_sub (a~1 + 1)%pos (b + 1)%pos = binint_pos_sub a~1%pos b
binint_pos_sub (a~1 + 1)%pos (b~0 + 1)%pos = binint_pos_sub a~1%pos b~0%pos
a: Pos
IHa: forall b0 : Pos,
binint_pos_sub (a + 1)%pos (b0 + 1)%pos = binint_pos_sub a b0
b: Pos
IHb: binint_pos_sub (a~1 + 1)%pos (b + 1)%pos = binint_pos_sub a~1%pos b
binint_pos_sub (a~1 + 1)%pos (b~1 + 1)%pos = binint_pos_sub a~1%pos b~1%pos
  {
b: Pos
IHb: binint_pos_sub (1 + 1)%pos (b + 1)%pos = binint_pos_sub 1%pos b
binint_pos_sub (1 + 1)%pos (b~1 + 1)%pos = binint_pos_sub 1%pos b~1%pos destruct b; trivial.
b: Pos
IHb: binint_pos_sub (1 + 1)%pos (b~1 + 1)%pos = binint_pos_sub 1%pos b~1%pos
binint_pos_sub (1 + 1)%pos (b~1~1 + 1)%pos = binint_pos_sub 1%pos b~1~1%pos
    cbn; apply ap.
b: Pos
IHb: binint_pos_sub (1 + 1)%pos (b~1 + 1)%pos = binint_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, binint_pos_sub (a + 1)%pos (b + 1)%pos = binint_pos_sub a b
binint_pos_sub (a~0 + 1)%pos (1 + 1)%pos = binint_pos_sub a~0%pos 1%pos
a: Pos
IHa: forall b0 : Pos,
binint_pos_sub (a + 1)%pos (b0 + 1)%pos = binint_pos_sub a b0
b: Pos
IHb: binint_pos_sub (a~0 + 1)%pos (b + 1)%pos = binint_pos_sub a~0%pos b
binint_pos_sub (a~0 + 1)%pos (b~1 + 1)%pos = binint_pos_sub a~0%pos b~1%pos
a: Pos
IHa: forall b : Pos, binint_pos_sub (a + 1)%pos (b + 1)%pos = binint_pos_sub a b
binint_pos_sub (a~1 + 1)%pos (1 + 1)%pos = binint_pos_sub a~1%pos 1%pos
a: Pos
IHa: forall b0 : Pos,
binint_pos_sub (a + 1)%pos (b0 + 1)%pos = binint_pos_sub a b0
b: Pos
IHb: binint_pos_sub (a~1 + 1)%pos (b + 1)%pos = binint_pos_sub a~1%pos b
binint_pos_sub (a~1 + 1)%pos (b~0 + 1)%pos = binint_pos_sub a~1%pos b~0%pos
a: Pos
IHa: forall b0 : Pos,
binint_pos_sub (a + 1)%pos (b0 + 1)%pos = binint_pos_sub a b0
b: Pos
IHb: binint_pos_sub (a~1 + 1)%pos (b + 1)%pos = binint_pos_sub a~1%pos b
binint_pos_sub (a~1 + 1)%pos (b~1 + 1)%pos = binint_pos_sub a~1%pos b~1%pos
  1: destruct a; trivial.
a: Pos
IHa: forall b0 : Pos,
binint_pos_sub (a + 1)%pos (b0 + 1)%pos = binint_pos_sub a b0
b: Pos
IHb: binint_pos_sub (a~0 + 1)%pos (b + 1)%pos = binint_pos_sub a~0%pos b
binint_pos_sub (a~0 + 1)%pos (b~1 + 1)%pos = binint_pos_sub a~0%pos b~1%pos
a: Pos
IHa: forall b : Pos, binint_pos_sub (a + 1)%pos (b + 1)%pos = binint_pos_sub a b
binint_pos_sub (a~1 + 1)%pos (1 + 1)%pos = binint_pos_sub a~1%pos 1%pos
a: Pos
IHa: forall b0 : Pos,
binint_pos_sub (a + 1)%pos (b0 + 1)%pos = binint_pos_sub a b0
b: Pos
IHb: binint_pos_sub (a~1 + 1)%pos (b + 1)%pos = binint_pos_sub a~1%pos b
binint_pos_sub (a~1 + 1)%pos (b~0 + 1)%pos = binint_pos_sub a~1%pos b~0%pos
a: Pos
IHa: forall b0 : Pos,
binint_pos_sub (a + 1)%pos (b0 + 1)%pos = binint_pos_sub a b0
b: Pos
IHb: binint_pos_sub (a~1 + 1)%pos (b + 1)%pos = binint_pos_sub a~1%pos b
binint_pos_sub (a~1 + 1)%pos (b~1 + 1)%pos = binint_pos_sub a~1%pos b~1%pos
  1: apply binint_succ_double_binint_pos_sub.
a: Pos
IHa: forall b : Pos, binint_pos_sub (a + 1)%pos (b + 1)%pos = binint_pos_sub a b
binint_pos_sub (a~1 + 1)%pos (1 + 1)%pos = binint_pos_sub a~1%pos 1%pos
a: Pos
IHa: forall b0 : Pos,
binint_pos_sub (a + 1)%pos (b0 + 1)%pos = binint_pos_sub a b0
b: Pos
IHb: binint_pos_sub (a~1 + 1)%pos (b + 1)%pos = binint_pos_sub a~1%pos b
binint_pos_sub (a~1 + 1)%pos (b~0 + 1)%pos = binint_pos_sub a~1%pos b~0%pos
a: Pos
IHa: forall b0 : Pos,
binint_pos_sub (a + 1)%pos (b0 + 1)%pos = binint_pos_sub a b0
b: Pos
IHb: binint_pos_sub (a~1 + 1)%pos (b + 1)%pos = binint_pos_sub a~1%pos b
binint_pos_sub (a~1 + 1)%pos (b~1 + 1)%pos = binint_pos_sub a~1%pos b~1%pos
  {
a: Pos
IHa: forall b : Pos, binint_pos_sub (a + 1)%pos (b + 1)%pos = binint_pos_sub a b
binint_pos_sub (a~1 + 1)%pos (1 + 1)%pos = binint_pos_sub a~1%pos 1%pos destruct a; trivial.
a: Pos
IHa: forall b : Pos,
binint_pos_sub (a~1 + 1)%pos (b + 1)%pos = binint_pos_sub a~1%pos b
binint_pos_sub (a~1~1 + 1)%pos (1 + 1)%pos = binint_pos_sub a~1~1%pos 1%pos
    cbn; apply ap, ap, pos_pred_double_succ. }
a: Pos
IHa: forall b0 : Pos,
binint_pos_sub (a + 1)%pos (b0 + 1)%pos = binint_pos_sub a b0
b: Pos
IHb: binint_pos_sub (a~1 + 1)%pos (b + 1)%pos = binint_pos_sub a~1%pos b
binint_pos_sub (a~1 + 1)%pos (b~0 + 1)%pos = binint_pos_sub a~1%pos b~0%pos
a: Pos
IHa: forall b0 : Pos,
binint_pos_sub (a + 1)%pos (b0 + 1)%pos = binint_pos_sub a b0
b: Pos
IHb: binint_pos_sub (a~1 + 1)%pos (b + 1)%pos = binint_pos_sub a~1%pos b
binint_pos_sub (a~1 + 1)%pos (b~1 + 1)%pos = binint_pos_sub a~1%pos b~1%pos
  1: apply binint_pred_double_binint_pos_sub.
a: Pos
IHa: forall b0 : Pos,
binint_pos_sub (a + 1)%pos (b0 + 1)%pos = binint_pos_sub a b0
b: Pos
IHb: binint_pos_sub (a~1 + 1)%pos (b + 1)%pos = binint_pos_sub a~1%pos b
binint_pos_sub (a~1 + 1)%pos (b~1 + 1)%pos = binint_pos_sub a~1%pos b~1%pos
  cbn; apply ap.
a: Pos
IHa: forall b0 : Pos,
binint_pos_sub (a + 1)%pos (b0 + 1)%pos = binint_pos_sub a b0
b: Pos
IHb: binint_pos_sub (a~1 + 1)%pos (b + 1)%pos = binint_pos_sub a~1%pos b
binint_pos_sub (pos_succ a) (pos_succ b) = binint_pos_sub a b
  rewrite <- 2 pos_add_1_r.
a: Pos
IHa: forall b0 : Pos,
binint_pos_sub (a + 1)%pos (b0 + 1)%pos = binint_pos_sub a b0
b: Pos
IHb: binint_pos_sub (a~1 + 1)%pos (b + 1)%pos = binint_pos_sub a~1%pos b
binint_pos_sub (a + 1)%pos (b + 1)%pos = binint_pos_sub a b
  apply IHa.
Defined.

(** ** Predecessor of a subtraction is the subtraction of a successor. *)
Lemma binint_pred_pos_sub_r a b
  : binint_pred (binint_pos_sub a b) = binint_pos_sub a (pos_succ b).
a, b: Pos
binint_pred (binint_pos_sub a b) = binint_pos_sub a (pos_succ b)
Proof.
a, b: Pos
binint_pred (binint_pos_sub a b) = binint_pos_sub a (pos_succ b)
  revert a.
b: Pos
forall a : Pos,
binint_pred (binint_pos_sub a b) = binint_pos_sub a (pos_succ b)
  induction b as [|b bH] using pos_peano_ind.
forall a : Pos,
binint_pred (binint_pos_sub a 1%pos) = binint_pos_sub a (pos_succ 1%pos)
b: Pos
bH: forall a : Pos,
binint_pred (binint_pos_sub a b) = binint_pos_sub a (pos_succ b)
forall a : Pos,
binint_pred (binint_pos_sub a (pos_succ b)) =
binint_pos_sub a (pos_succ (pos_succ b))
  1: destruct a; trivial; destruct a; trivial.
b: Pos
bH: forall a : Pos,
binint_pred (binint_pos_sub a b) = binint_pos_sub a (pos_succ b)
forall a : Pos,
binint_pred (binint_pos_sub a (pos_succ b)) =
binint_pos_sub a (pos_succ (pos_succ b))
  intro a.
b: Pos
bH: forall a0 : Pos,
binint_pred (binint_pos_sub a0 b) = binint_pos_sub a0 (pos_succ b)
a: Pos
binint_pred (binint_pos_sub a (pos_succ b)) =
binint_pos_sub a (pos_succ (pos_succ b))
  revert b bH.
a: Pos
forall b : Pos,
(forall a0 : Pos,
 binint_pred (binint_pos_sub a0 b) = binint_pos_sub a0 (pos_succ b)) ->
binint_pred (binint_pos_sub a (pos_succ b)) =
binint_pos_sub a (pos_succ (pos_succ b))
  induction a as [|a aH] using pos_peano_ind.
forall b : Pos,
(forall a : Pos,
 binint_pred (binint_pos_sub a b) = binint_pos_sub a (pos_succ b)) ->
binint_pred (binint_pos_sub 1%pos (pos_succ b)) =
binint_pos_sub 1%pos (pos_succ (pos_succ b))
a: Pos
aH: forall b : Pos,
(forall a0 : Pos,
 binint_pred (binint_pos_sub a0 b) = binint_pos_sub a0 (pos_succ b)) ->
binint_pred (binint_pos_sub a (pos_succ b)) =
binint_pos_sub a (pos_succ (pos_succ b))
forall b : Pos,
(forall a0 : Pos,
 binint_pred (binint_pos_sub a0 b) = binint_pos_sub a0 (pos_succ b)) ->
binint_pred (binint_pos_sub (pos_succ a) (pos_succ b)) =
binint_pos_sub (pos_succ a) (pos_succ (pos_succ b))
  {
forall b : Pos,
(forall a : Pos,
 binint_pred (binint_pos_sub a b) = binint_pos_sub a (pos_succ b)) ->
binint_pred (binint_pos_sub 1%pos (pos_succ b)) =
binint_pos_sub 1%pos (pos_succ (pos_succ b)) intros b bH.
b: Pos
bH: forall a : Pos,
binint_pred (binint_pos_sub a b) = binint_pos_sub a (pos_succ b)
binint_pred (binint_pos_sub 1%pos (pos_succ b)) =
binint_pos_sub 1%pos (pos_succ (pos_succ b))
    rewrite <- bH.
b: Pos
bH: forall a : Pos,
binint_pred (binint_pos_sub a b) = binint_pos_sub a (pos_succ b)
binint_pred (binint_pred (binint_pos_sub 1%pos b)) =
binint_pos_sub 1%pos (pos_succ (pos_succ b))
    destruct b; trivial.
b: Pos
bH: forall a : Pos,
binint_pred (binint_pos_sub a b~0%pos) = binint_pos_sub a (pos_succ b~0%pos)
binint_pred (binint_pred (binint_pos_sub 1%pos b~0%pos)) =
binint_pos_sub 1%pos (pos_succ (pos_succ b~0%pos))
    cbn; apply ap.
b: Pos
bH: forall a : Pos,
binint_pred (binint_pos_sub a b~0%pos) = binint_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,
binint_pred (binint_pos_sub a b~0%pos) = binint_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,
binint_pred (binint_pos_sub a b~0%pos) = binint_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,
binint_pred (binint_pos_sub a b~0%pos) = binint_pos_sub a (pos_succ b~0%pos)
pos_succ b~0%pos = b~1%pos
    trivial. }
a: Pos
aH: forall b : Pos,
(forall a0 : Pos,
 binint_pred (binint_pos_sub a0 b) = binint_pos_sub a0 (pos_succ b)) ->
binint_pred (binint_pos_sub a (pos_succ b)) =
binint_pos_sub a (pos_succ (pos_succ b))
forall b : Pos,
(forall a0 : Pos,
 binint_pred (binint_pos_sub a0 b) = binint_pos_sub a0 (pos_succ b)) ->
binint_pred (binint_pos_sub (pos_succ a) (pos_succ b)) =
binint_pos_sub (pos_succ a) (pos_succ (pos_succ b))
  intros b bH.
a: Pos
aH: forall b0 : Pos,
(forall a0 : Pos,
 binint_pred (binint_pos_sub a0 b0) = binint_pos_sub a0 (pos_succ b0)) ->
binint_pred (binint_pos_sub a (pos_succ b0)) =
binint_pos_sub a (pos_succ (pos_succ b0))
b: Pos
bH: forall a0 : Pos,
binint_pred (binint_pos_sub a0 b) = binint_pos_sub a0 (pos_succ b)
binint_pred (binint_pos_sub (pos_succ a) (pos_succ b)) =
binint_pos_sub (pos_succ a) (pos_succ (pos_succ b))
  rewrite 2 binint_pos_sub_succ_succ.
a: Pos
aH: forall b0 : Pos,
(forall a0 : Pos,
 binint_pred (binint_pos_sub a0 b0) = binint_pos_sub a0 (pos_succ b0)) ->
binint_pred (binint_pos_sub a (pos_succ b0)) =
binint_pos_sub a (pos_succ (pos_succ b0))
b: Pos
bH: forall a0 : Pos,
binint_pred (binint_pos_sub a0 b) = binint_pos_sub a0 (pos_succ b)
binint_pred (binint_pos_sub a b) = binint_pos_sub a (pos_succ b)
  apply bH.
Defined.

(** ** Negation of the predecessor is an involution. *)
Lemma binint_negation_pred_negation_red x
  : - binint_pred (- binint_pred x) = x.
x: BinInt
- binint_pred (- binint_pred x) = x
Proof.
x: BinInt
- binint_pred (- binint_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 binint_pred_add_r a b
  : binint_pred (a + b) = a + binint_pred b.
a, b: BinInt
binint_pred (a + b) = a + binint_pred b
Proof.
a, b: BinInt
binint_pred (a + b) = a + binint_pred b
  revert a b.
forall a b : BinInt, binint_pred (a + b) = a + binint_pred b
  intros [a| |a] [b| |b]; trivial.
a, b: Pos
binint_pred (neg a + neg b) = neg a + binint_pred (neg b)
a, b: Pos
binint_pred (neg a + pos b) = neg a + binint_pred (pos b)
a, b: Pos
binint_pred (pos a + neg b) = pos a + binint_pred (neg b)
a, b: Pos
binint_pred (pos a + pos b) = pos a + binint_pred (pos b)
  +
a, b: Pos
binint_pred (neg a + neg b) = neg a + binint_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
binint_pred (neg a + pos b) = neg a + binint_pred (pos b) revert a.
b: Pos
forall a : Pos, binint_pred (neg a + pos b) = neg a + binint_pred (pos b)
    induction b as [|b bH] using pos_peano_ind.
forall a : Pos, binint_pred (neg a + 1) = neg a + binint_pred 1
b: Pos
bH: forall a : Pos, binint_pred (neg a + pos b) = neg a + binint_pred (pos b)
forall a : Pos,
binint_pred (neg a + pos (pos_succ b)) =
neg a + binint_pred (pos (pos_succ b))
    -
forall a : Pos, binint_pred (neg a + 1) = neg a + binint_pred 1 intro a; exact (binint_pred_succ (neg a)).
    -
b: Pos
bH: forall a : Pos, binint_pred (neg a + pos b) = neg a + binint_pred (pos b)
forall a : Pos,
binint_pred (neg a + pos (pos_succ b)) =
neg a + binint_pred (pos (pos_succ b)) intro a.
b: Pos
bH: forall a0 : Pos, binint_pred (neg a0 + pos b) = neg a0 + binint_pred (pos b)
a: Pos
binint_pred (neg a + pos (pos_succ b)) =
neg a + binint_pred (pos (pos_succ b))
      rewrite <- pos_add_1_r.
b: Pos
bH: forall a0 : Pos, binint_pred (neg a0 + pos b) = neg a0 + binint_pred (pos b)
a: Pos
binint_pred (neg a + pos (b + 1%pos)) = neg a + binint_pred (pos (b + 1%pos))
      rewrite (binint_pred_succ (pos b)).
b: Pos
bH: forall a0 : Pos, binint_pred (neg a0 + pos b) = neg a0 + binint_pred (pos b)
a: Pos
binint_pred (neg a + pos (b + 1%pos)) = neg a + pos b
      rewrite binint_add_comm.
b: Pos
bH: forall a0 : Pos, binint_pred (neg a0 + pos b) = neg a0 + binint_pred (pos b)
a: Pos
binint_pred (pos (b + 1%pos) + neg a) = neg a + pos b
      cbn.
b: Pos
bH: forall a0 : Pos, binint_pred (neg a0 + pos b) = neg a0 + binint_pred (pos b)
a: Pos
binint_pred (binint_pos_sub (b + 1)%pos a) = binint_pos_sub b a
      rewrite pos_add_1_r.
b: Pos
bH: forall a0 : Pos, binint_pred (neg a0 + pos b) = neg a0 + binint_pred (pos b)
a: Pos
binint_pred (binint_pos_sub (pos_succ b) a) = binint_pos_sub b a
      rewrite <- binint_pos_sub_negation.
b: Pos
bH: forall a0 : Pos, binint_pred (neg a0 + pos b) = neg a0 + binint_pred (pos b)
a: Pos
binint_pred (- binint_pos_sub a (pos_succ b)) = binint_pos_sub b a
      rewrite <- binint_pred_pos_sub_r.
b: Pos
bH: forall a0 : Pos, binint_pred (neg a0 + pos b) = neg a0 + binint_pred (pos b)
a: Pos
binint_pred (- binint_pred (binint_pos_sub a b)) = binint_pos_sub b a
      apply binint_negation_inj.
b: Pos
bH: forall a0 : Pos, binint_pred (neg a0 + pos b) = neg a0 + binint_pred (pos b)
a: Pos
- binint_pred (- binint_pred (binint_pos_sub a b)) = - binint_pos_sub b a
      rewrite binint_pos_sub_negation.
b: Pos
bH: forall a0 : Pos, binint_pred (neg a0 + pos b) = neg a0 + binint_pred (pos b)
a: Pos
- binint_pred (- binint_pred (binint_pos_sub a b)) = binint_pos_sub a b
      apply binint_negation_pred_negation_red.
  +
a, b: Pos
binint_pred (pos a + neg b) = pos a + binint_pred (neg b) cbn.
a, b: Pos
binint_pred (binint_pos_sub a b) = binint_pos_sub a (b + 1)%pos
    rewrite pos_add_1_r.
a, b: Pos
binint_pred (binint_pos_sub a b) = binint_pos_sub a (pos_succ b)
    apply binint_pred_pos_sub_r.
  +
a, b: Pos
binint_pred (pos a + pos b) = pos a + binint_pred (pos b) revert a.
b: Pos
forall a : Pos, binint_pred (pos a + pos b) = pos a + binint_pred (pos b)
    induction b as [|b bH] using pos_peano_ind.
forall a : Pos, binint_pred (pos a + 1) = pos a + binint_pred 1
b: Pos
bH: forall a : Pos, binint_pred (pos a + pos b) = pos a + binint_pred (pos b)
forall a : Pos,
binint_pred (pos a + pos (pos_succ b)) =
pos a + binint_pred (pos (pos_succ b))
    -
forall a : Pos, binint_pred (pos a + 1) = pos a + binint_pred 1 intro a; exact (binint_pred_succ (pos a)).
    -
b: Pos
bH: forall a : Pos, binint_pred (pos a + pos b) = pos a + binint_pred (pos b)
forall a : Pos,
binint_pred (pos a + pos (pos_succ b)) =
pos a + binint_pred (pos (pos_succ b)) intro a.
b: Pos
bH: forall a0 : Pos, binint_pred (pos a0 + pos b) = pos a0 + binint_pred (pos b)
a: Pos
binint_pred (pos a + pos (pos_succ b)) =
pos a + binint_pred (pos (pos_succ b))
      rewrite <- pos_add_1_r.
b: Pos
bH: forall a0 : Pos, binint_pred (pos a0 + pos b) = pos a0 + binint_pred (pos b)
a: Pos
binint_pred (pos a + pos (b + 1%pos)) = pos a + binint_pred (pos (b + 1%pos))
      rewrite (binint_pred_succ (pos b)).
b: Pos
bH: forall a0 : Pos, binint_pred (pos a0 + pos b) = pos a0 + binint_pred (pos b)
a: Pos
binint_pred (pos a + pos (b + 1%pos)) = pos a + pos b
      cbn; rewrite pos_add_assoc.
b: Pos
bH: forall a0 : Pos, binint_pred (pos a0 + pos b) = pos a0 + binint_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 (binint_pred (binint_succ (pos (a + b)%pos)) = pos a + pos b).
b: Pos
bH: forall a0 : Pos, binint_pred (pos a0 + pos b) = pos a0 + binint_pred (pos b)
a: Pos
binint_pred (binint_succ (pos (a + b))) = pos a + pos b
      apply binint_pred_succ.
Defined.

(** ** Subtraction from a sum is the sum of a subtraction *)
Lemma binint_pos_sub_add (a b c : Pos)
  : binint_pos_sub (a + b)%pos c = pos a + binint_pos_sub b c.
a, b, c: Pos
binint_pos_sub (a + b)%pos c = pos a + binint_pos_sub b c
Proof.
a, b, c: Pos
binint_pos_sub (a + b)%pos c = pos a + binint_pos_sub b c
  revert c b a.
forall c b a : Pos, binint_pos_sub (a + b)%pos c = pos a + binint_pos_sub b c
  induction c as [|c ch] using pos_peano_ind.
forall b a : Pos,
binint_pos_sub (a + b)%pos 1%pos = pos a + binint_pos_sub b 1%pos
c: Pos
ch: forall b a : Pos, binint_pos_sub (a + b)%pos c = pos a + binint_pos_sub b c
forall b a : Pos,
binint_pos_sub (a + b)%pos (pos_succ c) =
pos a + binint_pos_sub b (pos_succ c)
  {
forall b a : Pos,
binint_pos_sub (a + b)%pos 1%pos = pos a + binint_pos_sub b 1%pos intros b a.
b, a: Pos
binint_pos_sub (a + b)%pos 1%pos = pos a + binint_pos_sub b 1%pos
    change (binint_pred (pos a + pos b) = pos a + (binint_pred (pos b))).
b, a: Pos
binint_pred (pos a + pos b) = pos a + binint_pred (pos b)
    apply binint_pred_add_r. }
c: Pos
ch: forall b a : Pos, binint_pos_sub (a + b)%pos c = pos a + binint_pos_sub b c
forall b a : Pos,
binint_pos_sub (a + b)%pos (pos_succ c) =
pos a + binint_pos_sub b (pos_succ c)
  intros b a.
c: Pos
ch: forall b0 a0 : Pos,
binint_pos_sub (a0 + b0)%pos c = pos a0 + binint_pos_sub b0 c
b, a: Pos
binint_pos_sub (a + b)%pos (pos_succ c) =
pos a + binint_pos_sub b (pos_succ c)
  rewrite <- binint_pred_pos_sub_r.
c: Pos
ch: forall b0 a0 : Pos,
binint_pos_sub (a0 + b0)%pos c = pos a0 + binint_pos_sub b0 c
b, a: Pos
binint_pred (binint_pos_sub (a + b)%pos c) =
pos a + binint_pos_sub b (pos_succ c)
  rewrite ch.
c: Pos
ch: forall b0 a0 : Pos,
binint_pos_sub (a0 + b0)%pos c = pos a0 + binint_pos_sub b0 c
b, a: Pos
binint_pred (pos a + binint_pos_sub b c) =
pos a + binint_pos_sub b (pos_succ c)
  rewrite <- binint_pred_pos_sub_r.
c: Pos
ch: forall b0 a0 : Pos,
binint_pos_sub (a0 + b0)%pos c = pos a0 + binint_pos_sub b0 c
b, a: Pos
binint_pred (pos a + binint_pos_sub b c) =
pos a + binint_pred (binint_pos_sub b c)
  apply binint_pred_add_r.
Defined.

(** An auxiliary lemma used to prove associativity. *)
Lemma binint_add_assoc_pos p n m : pos p + (n + m) = pos p + n + m.
p: Pos
n, m: BinInt
pos p + (n + m) = pos p + n + m
Proof.
p: Pos
n, m: BinInt
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 binint_negation_inj.
p, n, m: Pos
- binint_pos_sub p (n + m)%pos = - (binint_pos_sub p n + neg m)
    rewrite !binint_negation_add_distr, !binint_pos_sub_negation.
p, n, m: Pos
binint_pos_sub (n + m)%pos p = binint_pos_sub n p + - neg m
    rewrite binint_add_comm, pos_add_comm.
p, n, m: Pos
binint_pos_sub (m + n)%pos p = - neg m + binint_pos_sub n p
    apply binint_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 binint_add_0_r.
  -
p, n, m: Pos
pos p + (neg n + pos m) = pos p + neg n + pos m by rewrite <- binint_pos_sub_add, binint_add_comm,
      <- binint_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 binint_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 binint_add_assoc n m p : n + (m + p) = n + m + p.
n, m, p: BinInt
n + (m + p) = n + m + p
Proof.
n, m, p: BinInt
n + (m + p) = n + m + p
  destruct n.
p0: Pos
m, p: BinInt
neg p0 + (m + p) = neg p0 + m + p
m, p: BinInt
0 + (m + p) = 0 + m + p
p0: Pos
m, p: BinInt
pos p0 + (m + p) = pos p0 + m + p
  -
p0: Pos
m, p: BinInt
neg p0 + (m + p) = neg p0 + m + p apply binint_negation_inj.
p0: Pos
m, p: BinInt
- (neg p0 + (m + p)) = - (neg p0 + m + p)
    rewrite !binint_negation_add_distr.
p0: Pos
m, p: BinInt
- neg p0 + (- m + - p) = - neg p0 + - m + - p
    apply binint_add_assoc_pos.
  -
m, p: BinInt
0 + (m + p) = 0 + m + p trivial.
  -
p0: Pos
m, p: BinInt
pos p0 + (m + p) = pos p0 + m + p apply binint_add_assoc_pos.
Defined.

(** ** Relationship between [int_succ], [int_pred] and addition. *)
Lemma binint_add_succ_l a b : binint_succ a + b = binint_succ (a + b).
a, b: BinInt
binint_succ a + b = binint_succ (a + b)
Proof.
a, b: BinInt
binint_succ a + b = binint_succ (a + b)
  rewrite <- binint_add_assoc, (binint_add_comm 1 b).
a, b: BinInt
a + (b + 1) = binint_succ (a + b)
  apply binint_add_assoc.
Defined.

Lemma binint_add_succ_r a b : a + binint_succ b = binint_succ (a + b).
a, b: BinInt
a + binint_succ b = binint_succ (a + b)
Proof.
a, b: BinInt
a + binint_succ b = binint_succ (a + b)
  apply binint_add_assoc.
Defined.

Lemma binint_add_pred_l a b : binint_pred a + b = binint_pred (a + b).
a, b: BinInt
binint_pred a + b = binint_pred (a + b)
Proof.
a, b: BinInt
binint_pred a + b = binint_pred (a + b)
  rewrite <- binint_add_assoc, (binint_add_comm (-1) b).
a, b: BinInt
a + (b + -1) = binint_pred (a + b)
  apply binint_add_assoc.
Defined.

Lemma binint_add_pred_r a b : a + binint_pred b = binint_pred (a + b).
a, b: BinInt
a + binint_pred b = binint_pred (a + b)
Proof.
a, b: BinInt
a + binint_pred b = binint_pred (a + b)
  apply binint_add_assoc.
Defined.

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

(** Distributivity of multiplication over addition *)

Lemma binint_pos_sub_mul_pos n m p
  : binint_pos_sub n m * pos p = binint_pos_sub (n * p)%pos (m * p)%pos.
n, m, p: Pos
binint_pos_sub n m * pos p = binint_pos_sub (n * p)%pos (m * p)%pos
Proof.
n, m, p: Pos
binint_pos_sub n m * pos p = binint_pos_sub (n * p)%pos (m * p)%pos
  rewrite binint_mul_comm.
n, m, p: Pos
pos p * binint_pos_sub n m = binint_pos_sub (n * p)%pos (m * p)%pos
  rewrite 2 (pos_mul_comm _ p).
n, m, p: Pos
pos p * binint_pos_sub n m = binint_pos_sub (p * n)%pos (p * m)%pos
  induction p.
n, m: Pos
1 * binint_pos_sub n m = binint_pos_sub (1 * n)%pos (1 * m)%pos
n, m, p: Pos
IHp: pos p * binint_pos_sub n m = binint_pos_sub (p * n)%pos (p * m)%pos
pos p~0 * binint_pos_sub n m = binint_pos_sub (p~0 * n)%pos (p~0 * m)%pos
n, m, p: Pos
IHp: pos p * binint_pos_sub n m = binint_pos_sub (p * n)%pos (p * m)%pos
pos p~1 * binint_pos_sub n m = binint_pos_sub (p~1 * n)%pos (p~1 * m)%pos
  {
n, m: Pos
1 * binint_pos_sub n m = binint_pos_sub (1 * n)%pos (1 * m)%pos rewrite 2 pos_mul_1_l.
n, m: Pos
1 * binint_pos_sub n m = binint_pos_sub n m
    apply binint_mul_1_l. }
n, m, p: Pos
IHp: pos p * binint_pos_sub n m = binint_pos_sub (p * n)%pos (p * m)%pos
pos p~0 * binint_pos_sub n m = binint_pos_sub (p~0 * n)%pos (p~0 * m)%pos
n, m, p: Pos
IHp: pos p * binint_pos_sub n m = binint_pos_sub (p * n)%pos (p * m)%pos
pos p~1 * binint_pos_sub n m = binint_pos_sub (p~1 * n)%pos (p~1 * m)%pos
  {
n, m, p: Pos
IHp: pos p * binint_pos_sub n m = binint_pos_sub (p * n)%pos (p * m)%pos
pos p~0 * binint_pos_sub n m = binint_pos_sub (p~0 * n)%pos (p~0 * m)%pos cbn.
n, m, p: Pos
IHp: pos p * binint_pos_sub n m = binint_pos_sub (p * n)%pos (p * m)%pos
match binint_pos_sub n m with
| neg y' => neg (p * y')~0%pos
| 0 => 0
| pos y' => pos (p * y')%pos~0
end = binint_double (binint_pos_sub (p * n)%pos (p * m)%pos)
    rewrite <- IHp.
n, m, p: Pos
IHp: pos p * binint_pos_sub n m = binint_pos_sub (p * n)%pos (p * m)%pos
match binint_pos_sub n m with
| neg y' => neg (p * y')~0%pos
| 0 => 0
| pos y' => pos (p * y')%pos~0
end = binint_double (pos p * binint_pos_sub n m)
    set (binint_pos_sub n m) as k.
n, m, p: Pos
IHp: pos p * binint_pos_sub n m = binint_pos_sub (p * n)%pos (p * m)%pos
k:= binint_pos_sub n m: BinInt
match k with
| neg y' => neg (p * y')~0%pos
| 0 => 0
| pos y' => pos (p * y')%pos~0
end = binint_double (pos p * k)
    by destruct k. }
n, m, p: Pos
IHp: pos p * binint_pos_sub n m = binint_pos_sub (p * n)%pos (p * m)%pos
pos p~1 * binint_pos_sub n m = binint_pos_sub (p~1 * n)%pos (p~1 * m)%pos
  cbn.
n, m, p: Pos
IHp: pos p * binint_pos_sub n m = binint_pos_sub (p * n)%pos (p * m)%pos
match binint_pos_sub n m with
| neg y' => neg (y' + (p * y')~0)%pos
| 0 => 0
| pos y' => pos (y' + (p * y')~0%pos)
end = binint_pos_sub (n + (p * n)~0)%pos (m + (p * m)~0)%pos
  rewrite binint_pos_sub_add.
n, m, p: Pos
IHp: pos p * binint_pos_sub n m = binint_pos_sub (p * n)%pos (p * m)%pos
match binint_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 + binint_pos_sub (p * n)~0%pos (m + (p * m)~0)%pos
  rewrite <- (binint_pos_sub_negation _ (x0 _)).
n, m, p: Pos
IHp: pos p * binint_pos_sub n m = binint_pos_sub (p * n)%pos (p * m)%pos
match binint_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 + - binint_pos_sub (m + (p * m)~0)%pos (p * n)~0%pos
  rewrite binint_pos_sub_add.
n, m, p: Pos
IHp: pos p * binint_pos_sub n m = binint_pos_sub (p * n)%pos (p * m)%pos
match binint_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 + binint_pos_sub (p * m)~0%pos (p * n)~0%pos)
  rewrite binint_negation_add_distr.
n, m, p: Pos
IHp: pos p * binint_pos_sub n m = binint_pos_sub (p * n)%pos (p * m)%pos
match binint_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 + - binint_pos_sub (p * m)~0%pos (p * n)~0%pos)
  rewrite binint_pos_sub_negation.
n, m, p: Pos
IHp: pos p * binint_pos_sub n m = binint_pos_sub (p * n)%pos (p * m)%pos
match binint_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 + binint_pos_sub (p * n)~0%pos (p * m)~0%pos)
  rewrite binint_add_assoc.
n, m, p: Pos
IHp: pos p * binint_pos_sub n m = binint_pos_sub (p * n)%pos (p * m)%pos
match binint_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 + binint_pos_sub (p * n)~0%pos (p * m)~0%pos
  cbn.
n, m, p: Pos
IHp: pos p * binint_pos_sub n m = binint_pos_sub (p * n)%pos (p * m)%pos
match binint_pos_sub n m with
| neg y' => neg (y' + (p * y')~0)%pos
| 0 => 0
| pos y' => pos (y' + (p * y')~0%pos)
end =
binint_pos_sub n m + binint_double (binint_pos_sub (p * n)%pos (p * m)%pos)
  rewrite <- IHp.
n, m, p: Pos
IHp: pos p * binint_pos_sub n m = binint_pos_sub (p * n)%pos (p * m)%pos
match binint_pos_sub n m with
| neg y' => neg (y' + (p * y')~0)%pos
| 0 => 0
| pos y' => pos (y' + (p * y')~0%pos)
end = binint_pos_sub n m + binint_double (pos p * binint_pos_sub n m)
  set (binint_pos_sub n m) as k.
n, m, p: Pos
IHp: pos p * binint_pos_sub n m = binint_pos_sub (p * n)%pos (p * m)%pos
k:= binint_pos_sub n m: BinInt
match k with
| neg y' => neg (y' + (p * y')~0)%pos
| 0 => 0
| pos y' => pos (y' + (p * y')~0%pos)
end = k + binint_double (pos p * k)
  by destruct k.
Defined.

Lemma binint_pos_sub_mul_neg n m p
  : binint_pos_sub m n  * neg p = binint_pos_sub (n * p)%pos (m * p)%pos.
n, m, p: Pos
binint_pos_sub m n * neg p = binint_pos_sub (n * p)%pos (m * p)%pos
Proof.
n, m, p: Pos
binint_pos_sub m n * neg p = binint_pos_sub (n * p)%pos (m * p)%pos
  rewrite binint_mul_comm.
n, m, p: Pos
neg p * binint_pos_sub m n = binint_pos_sub (n * p)%pos (m * p)%pos
  rewrite 2 (pos_mul_comm _ p).
n, m, p: Pos
neg p * binint_pos_sub m n = binint_pos_sub (p * n)%pos (p * m)%pos
  induction p.
n, m: Pos
-1 * binint_pos_sub m n = binint_pos_sub (1 * n)%pos (1 * m)%pos
n, m, p: Pos
IHp: neg p * binint_pos_sub m n = binint_pos_sub (p * n)%pos (p * m)%pos
neg p~0%pos * binint_pos_sub m n = binint_pos_sub (p~0 * n)%pos (p~0 * m)%pos
n, m, p: Pos
IHp: neg p * binint_pos_sub m n = binint_pos_sub (p * n)%pos (p * m)%pos
neg p~1%pos * binint_pos_sub m n = binint_pos_sub (p~1 * n)%pos (p~1 * m)%pos
  {
n, m: Pos
-1 * binint_pos_sub m n = binint_pos_sub (1 * n)%pos (1 * m)%pos rewrite 2 pos_mul_1_l.
n, m: Pos
-1 * binint_pos_sub m n = binint_pos_sub n m
    rewrite <- binint_pos_sub_negation.
n, m: Pos
-1 * - binint_pos_sub n m = binint_pos_sub n m
    by destruct (binint_pos_sub n m). }
n, m, p: Pos
IHp: neg p * binint_pos_sub m n = binint_pos_sub (p * n)%pos (p * m)%pos
neg p~0%pos * binint_pos_sub m n = binint_pos_sub (p~0 * n)%pos (p~0 * m)%pos
n, m, p: Pos
IHp: neg p * binint_pos_sub m n = binint_pos_sub (p * n)%pos (p * m)%pos
neg p~1%pos * binint_pos_sub m n = binint_pos_sub (p~1 * n)%pos (p~1 * m)%pos
  {
n, m, p: Pos
IHp: neg p * binint_pos_sub m n = binint_pos_sub (p * n)%pos (p * m)%pos
neg p~0%pos * binint_pos_sub m n = binint_pos_sub (p~0 * n)%pos (p~0 * m)%pos cbn.
n, m, p: Pos
IHp: neg p * binint_pos_sub m n = binint_pos_sub (p * n)%pos (p * m)%pos
match binint_pos_sub m n with
| neg y' => pos (p * y')%pos~0
| 0 => 0
| pos y' => neg (p * y')~0%pos
end = binint_double (binint_pos_sub (p * n)%pos (p * m)%pos)
    rewrite <- IHp.
n, m, p: Pos
IHp: neg p * binint_pos_sub m n = binint_pos_sub (p * n)%pos (p * m)%pos
match binint_pos_sub m n with
| neg y' => pos (p * y')%pos~0
| 0 => 0
| pos y' => neg (p * y')~0%pos
end = binint_double (neg p * binint_pos_sub m n)
    rewrite <- binint_pos_sub_negation.
n, m, p: Pos
IHp: neg p * binint_pos_sub m n = binint_pos_sub (p * n)%pos (p * m)%pos
match - binint_pos_sub n m with
| neg y' => pos (p * y')%pos~0
| 0 => 0
| pos y' => neg (p * y')~0%pos
end = binint_double (neg p * - binint_pos_sub n m)
    set (binint_pos_sub n m) as k.
n, m, p: Pos
IHp: neg p * binint_pos_sub m n = binint_pos_sub (p * n)%pos (p * m)%pos
k:= binint_pos_sub n m: BinInt
match - k with
| neg y' => pos (p * y')%pos~0
| 0 => 0
| pos y' => neg (p * y')~0%pos
end = binint_double (neg p * - k)
    by destruct k. }
n, m, p: Pos
IHp: neg p * binint_pos_sub m n = binint_pos_sub (p * n)%pos (p * m)%pos
neg p~1%pos * binint_pos_sub m n = binint_pos_sub (p~1 * n)%pos (p~1 * m)%pos
  cbn.
n, m, p: Pos
IHp: neg p * binint_pos_sub m n = binint_pos_sub (p * n)%pos (p * m)%pos
match binint_pos_sub m n with
| neg y' => pos (y' + (p * y')~0%pos)
| 0 => 0
| pos y' => neg (y' + (p * y')~0)%pos
end = binint_pos_sub (n + (p * n)~0)%pos (m + (p * m)~0)%pos
  rewrite binint_pos_sub_add.
n, m, p: Pos
IHp: neg p * binint_pos_sub m n = binint_pos_sub (p * n)%pos (p * m)%pos
match binint_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 + binint_pos_sub (p * n)~0%pos (m + (p * m)~0)%pos
  rewrite <- (binint_pos_sub_negation _ (x0 _)).
n, m, p: Pos
IHp: neg p * binint_pos_sub m n = binint_pos_sub (p * n)%pos (p * m)%pos
match binint_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 + - binint_pos_sub (m + (p * m)~0)%pos (p * n)~0%pos
  rewrite binint_pos_sub_add.
n, m, p: Pos
IHp: neg p * binint_pos_sub m n = binint_pos_sub (p * n)%pos (p * m)%pos
match binint_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 + binint_pos_sub (p * m)~0%pos (p * n)~0%pos)
  rewrite binint_negation_add_distr.
n, m, p: Pos
IHp: neg p * binint_pos_sub m n = binint_pos_sub (p * n)%pos (p * m)%pos
match binint_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 + - binint_pos_sub (p * m)~0%pos (p * n)~0%pos)
  rewrite binint_pos_sub_negation.
n, m, p: Pos
IHp: neg p * binint_pos_sub m n = binint_pos_sub (p * n)%pos (p * m)%pos
match binint_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 + binint_pos_sub (p * n)~0%pos (p * m)~0%pos)
  rewrite binint_add_assoc.
n, m, p: Pos
IHp: neg p * binint_pos_sub m n = binint_pos_sub (p * n)%pos (p * m)%pos
match binint_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 + binint_pos_sub (p * n)~0%pos (p * m)~0%pos
  cbn.
n, m, p: Pos
IHp: neg p * binint_pos_sub m n = binint_pos_sub (p * n)%pos (p * m)%pos
match binint_pos_sub m n with
| neg y' => pos (y' + (p * y')~0%pos)
| 0 => 0
| pos y' => neg (y' + (p * y')~0)%pos
end =
binint_pos_sub n m + binint_double (binint_pos_sub (p * n)%pos (p * m)%pos)
  rewrite <- IHp.
n, m, p: Pos
IHp: neg p * binint_pos_sub m n = binint_pos_sub (p * n)%pos (p * m)%pos
match binint_pos_sub m n with
| neg y' => pos (y' + (p * y')~0%pos)
| 0 => 0
| pos y' => neg (y' + (p * y')~0)%pos
end = binint_pos_sub n m + binint_double (neg p * binint_pos_sub m n)
  rewrite <- (binint_pos_sub_negation m).
n, m, p: Pos
IHp: neg p * binint_pos_sub m n = binint_pos_sub (p * n)%pos (p * m)%pos
match binint_pos_sub m n with
| neg y' => pos (y' + (p * y')~0%pos)
| 0 => 0
| pos y' => neg (y' + (p * y')~0)%pos
end = - binint_pos_sub m n + binint_double (neg p * binint_pos_sub m n)
  set (binint_pos_sub m n) as k.
n, m, p: Pos
IHp: neg p * binint_pos_sub m n = binint_pos_sub (p * n)%pos (p * m)%pos
k:= binint_pos_sub m n: BinInt
match k with
| neg y' => pos (y' + (p * y')~0%pos)
| 0 => 0
| pos y' => neg (y' + (p * y')~0)%pos
end = - k + binint_double (neg p * k)
  by destruct k.
Defined.

Lemma binint_mul_add_distr_r n m p : (n + m) * p = n * p + m * p.
n, m, p: BinInt
(n + m) * p = n * p + m * p
Proof.
n, m, p: BinInt
(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 binint_pos_sub_mul_neg;
  try apply binint_pos_sub_mul_pos;
  apply binint_mul_0_r.
Defined.

Lemma binint_mul_add_distr_l n m p : n * (m + p) = n * m + n * p.
n, m, p: BinInt
n * (m + p) = n * m + n * p
Proof.
n, m, p: BinInt
n * (m + p) = n * m + n * p
  rewrite 3 (binint_mul_comm n); apply binint_mul_add_distr_r.
Defined.

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