Require Import
        HoTT.Spaces.Nat.Core.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import
        HoTT.Tactics.
Require Import
        HoTT.Classes.interfaces.abstract_algebra
        HoTT.Classes.interfaces.naturals
        HoTT.Classes.interfaces.orders
        HoTT.Classes.implementations.peano_naturals
        HoTT.Classes.theory.rings
        HoTT.Classes.orders.semirings
        HoTT.Classes.theory.apartness.

Section basics.

  (* This definition of binary naturals is due to Martín Escardó and
     Cory Knapp *)

  Inductive binnat : Type0 :=
  | bzero   :           binnat  (* zero *)
  | double1 : binnat -> binnat  (* 2n+1 *)
  | double2 : binnat -> binnat. (* 2n+2 *)

  Fixpoint Succ (n : binnat) : binnat :=
    match n with
    | bzero      => double1 bzero
    | double1 n' => double2 n'
    | double2 n' => double1 (Succ n')
    end.

  Fixpoint double (n : binnat) : binnat :=
    match n with
    | bzero      => bzero
    | double1 n' => double2 (double n')
    | double2 n' => double2 (Succ (double n'))
    end.

  Fixpoint Double (n : nat) : nat :=
    match n with
    | O    => O
    | S n' => S (S (Double n'))
    end.

  Definition Double1 (n : nat) : nat := S (Double n).

  Definition Double2 (n : nat) : nat := S (S (Double n)).

  Fixpoint binary (n : nat) : binnat :=
    match n with
    | O    => bzero
    | S n' => Succ (binary n')
    end.

End basics.

Section binary_equiv.

  Local Fixpoint unary' (n : binnat) : nat :=
    match n with
    | bzero      => O
    | double1 n' => Double1 (unary' n')
    | double2 n' => Double2 (unary' n')
    end.

  Local Definition succunary (n : binnat) : unary' (Succ n) = S (unary' n).
n: binnat
unary' (Succ n) = (unary' n).+1%nat
  Proof.
n: binnat
unary' (Succ n) = (unary' n).+1%nat
    induction n.
unary' (Succ bzero) = (unary' bzero).+1%nat
n: binnat
IHn: unary' (Succ n) = (unary' n).+1%nat
unary' (Succ (double1 n)) =
(unary' (double1 n)).+1%nat
n: binnat
IHn: unary' (Succ n) = (unary' n).+1%nat
unary' (Succ (double2 n)) =
(unary' (double2 n)).+1%nat
    -
unary' (Succ bzero) = (unary' bzero).+1%nat reflexivity.
    -
n: binnat
IHn: unary' (Succ n) = (unary' n).+1%nat
unary' (Succ (double1 n)) =
(unary' (double1 n)).+1%nat reflexivity.
    -
n: binnat
IHn: unary' (Succ n) = (unary' n).+1%nat
unary' (Succ (double2 n)) =
(unary' (double2 n)).+1%nat simpl.
n: binnat
IHn: unary' (Succ n) = (unary' n).+1%nat
Double1 (unary' (Succ n)) =
(Double2 (unary' n)).+1%nat rewrite IHn.
n: binnat
IHn: unary' (Succ n) = (unary' n).+1%nat
Double1 (unary' n).+1 = (Double2 (unary' n)).+1%nat reflexivity.
  Qed.

  Local Definition unarybinary : unary' o binary == idmap.
unary' o binary == idmap
  Proof.
unary' o binary == idmap
    intros n; induction n as [|n IHn].
unary' (binary 0) = 0%nat
n: nat
IHn: unary' (binary n) = n
unary' (binary n.+1) = n.+1%nat
    -
unary' (binary 0) = 0%nat reflexivity.
    -
n: nat
IHn: unary' (binary n) = n
unary' (binary n.+1) = n.+1%nat simpl.
n: nat
IHn: unary' (binary n) = n
unary' (Succ (binary n)) = n.+1%nat rewrite succunary.
n: nat
IHn: unary' (binary n) = n
(unary' (binary n)).+1%nat = n.+1%nat apply ap.
n: nat
IHn: unary' (binary n) = n
unary' (binary n) = n exact IHn.
  Qed.

  Definition double1binary (n : nat) : binary (Double1 n) = double1 (binary n).
n: nat
binary (Double1 n) = double1 (binary n)
  Proof.
n: nat
binary (Double1 n) = double1 (binary n)
    induction n.
binary (Double1 0) = double1 (binary 0)
n: nat
IHn: binary (Double1 n) = double1 (binary n)
binary (Double1 n.+1) = double1 (binary n.+1)
    -
binary (Double1 0) = double1 (binary 0) reflexivity.
    -
n: nat
IHn: binary (Double1 n) = double1 (binary n)
binary (Double1 n.+1) = double1 (binary n.+1) change (binary (Double1 n.+1)) with (Succ (Succ (binary (Double n).+1))).
n: nat
IHn: binary (Double1 n) = double1 (binary n)
Succ (Succ (binary (Double n).+1)) =
double1 (binary n.+1)
      rewrite IHn.
n: nat
IHn: binary (Double1 n) = double1 (binary n)
Succ (Succ (double1 (binary n))) =
double1 (binary n.+1) reflexivity.
  Qed.

  Definition double2binary (n : nat) : binary (Double2 n) = double2 (binary n).
n: nat
binary (Double2 n) = double2 (binary n)
  Proof.
n: nat
binary (Double2 n) = double2 (binary n)
    induction n.
binary (Double2 0) = double2 (binary 0)
n: nat
IHn: binary (Double2 n) = double2 (binary n)
binary (Double2 n.+1) = double2 (binary n.+1)
    -
binary (Double2 0) = double2 (binary 0) reflexivity.
    -
n: nat
IHn: binary (Double2 n) = double2 (binary n)
binary (Double2 n.+1) = double2 (binary n.+1) change (binary (Double2 n.+1)) with (Succ (Succ (binary (Double n).+2))).
n: nat
IHn: binary (Double2 n) = double2 (binary n)
Succ (Succ (binary (Double n).+2)) =
double2 (binary n.+1)
      rewrite IHn.
n: nat
IHn: binary (Double2 n) = double2 (binary n)
Succ (Succ (double2 (binary n))) =
double2 (binary n.+1) reflexivity.
  Qed.

  Local Definition binaryunary : binary o unary' == idmap.
binary o unary' == idmap
  Proof.
binary o unary' == idmap
    intros n; induction n.
binary (unary' bzero) = bzero
n: binnat
IHn: binary (unary' n) = n
binary (unary' (double1 n)) = double1 n
n: binnat
IHn: binary (unary' n) = n
binary (unary' (double2 n)) = double2 n
    -
binary (unary' bzero) = bzero reflexivity.
    -
n: binnat
IHn: binary (unary' n) = n
binary (unary' (double1 n)) = double1 n rewrite double1binary.
n: binnat
IHn: binary (unary' n) = n
double1
  (binary
     ((fix unary' (n : binnat) : nat :=
         match n with
         | bzero => 0%nat
         | double1 n' => Double1 (unary' n')
         | double2 n' => Double2 (unary' n')
         end) n)) = double1 n apply ap.
n: binnat
IHn: binary (unary' n) = n
binary
  ((fix unary' (n : binnat) : nat :=
      match n with
      | bzero => 0%nat
      | double1 n' => Double1 (unary' n')
      | double2 n' => Double2 (unary' n')
      end) n) = n exact IHn.
    -
n: binnat
IHn: binary (unary' n) = n
binary (unary' (double2 n)) = double2 n rewrite double2binary.
n: binnat
IHn: binary (unary' n) = n
double2
  (binary
     ((fix unary' (n : binnat) : nat :=
         match n with
         | bzero => 0%nat
         | double1 n' => Double1 (unary' n')
         | double2 n' => Double2 (unary' n')
         end) n)) = double2 n apply ap.
n: binnat
IHn: binary (unary' n) = n
binary
  ((fix unary' (n : binnat) : nat :=
      match n with
      | bzero => 0%nat
      | double1 n' => Double1 (unary' n')
      | double2 n' => Double2 (unary' n')
      end) n) = n exact IHn.
  Qed.

  #[export] Instance isequiv_binary : IsEquiv binary :=
    isequiv_adjointify binary unary' binaryunary unarybinary.

  Definition equiv_binary : nat <~> binnat :=
    Build_Equiv _ _  binary isequiv_binary.

End binary_equiv.

Notation equiv_unary  := equiv_binary ^-1.
Notation unary := equiv_unary.

Section semiring_struct.

  #[export] Instance binnat_0 : Zero binnat := bzero.
  #[export] Instance binnat_1 : One binnat := double1 bzero.

  Local Fixpoint binnat_plus' (m n : binnat) : binnat :=
    match m, n with
    | bzero      , n'         => n'
    | double1 m' , bzero      => double1 m'
    (* compute m + n as 2m'+1 + 2n'+1 = 2(m'+n') + 2 *)
    | double1 m' , double1 n' => double2 (binnat_plus' m' n')
    (* compute m + n as 2m'+1 + 2n'+2 = 2(m'+n')+2 + 1 = 2(m' + n' + 1) + 1 *)
    | double1 m' , double2 n' => double1 (Succ (binnat_plus' m' n'))
    | double2 m' , bzero      => double2 m'
    (* compute m + n as 2m'+2 + 2n'+1 = 2(m'+n')+2 + 1 = 2(m' + n' + 1) + 1 *)
    | double2 m' , double1 n' => double1 (Succ (binnat_plus' m' n'))
    (* compute m + n as 2m'+2 + 2n'+2 = 2(m'+n')+2 + 2 = 2(m' + n' + 1) + 2*)
    | double2 m' , double2 n' => double2 (Succ (binnat_plus' m' n'))
    end.
  #[export] Instance binnat_plus : Plus binnat := binnat_plus'.

  Local Fixpoint binnat_mult' (m n : binnat) : binnat :=
    match m with
    | bzero      => bzero
    (* compute (2m'+1)*n as 2m'n+n *)
    | double1 m' => (binnat_mult' m' n) + (binnat_mult' m' n) + n
    | double2 m' => (binnat_mult' m' n) + (binnat_mult' m' n) + n + n
    end.
  #[export] Instance binnat_mult : Mult binnat := binnat_mult'.

End semiring_struct.

Section semiring_laws.

  Definition binarysucc (n : nat) : binary n.+1 = Succ (binary n).
n: nat
binary n.+1 = Succ (binary n)
  Proof.
n: nat
binary n.+1 = Succ (binary n)
    reflexivity.
  Qed.

  Definition unarysucc : forall m, unary (Succ m) = S (unary m).
forall m : binnat,
binary^-1 (Succ m) = (binary^-1 m).+1%nat
  Proof.
forall m : binnat,
binary^-1 (Succ m) = (binary^-1 m).+1%nat
    equiv_intros binary n.
n: nat
binary^-1 (Succ (binary n)) =
(binary^-1 (binary n)).+1%nat
    rewrite <- binarysucc.
n: nat
binary^-1 (binary n.+1) =
(binary^-1 (binary n)).+1%nat
    rewrite eissect, eissect.
n: nat
n.+1%nat = n.+1%nat
    reflexivity.
  Qed.

  Definition binnatplussucc : forall (m n : binnat), (Succ m) + n = Succ (m + n).
forall m n : binnat, Succ m + n = Succ (m + n)
  Proof.
forall m n : binnat, Succ m + n = Succ (m + n)
    induction m; induction n; try reflexivity; simpl; rewrite <- IHm; done.
  Qed.

  Definition binaryplus (m n : nat) : binary m + binary n = binary (m + n).
m, n: nat
binary m + binary n = binary (m + n)
  Proof.
m, n: nat
binary m + binary n = binary (m + n)
    induction m; induction n; try reflexivity.
m: nat
IHm: binary m + binary 0 = binary (m + 0)
binary m.+1 + binary 0 = binary (m.+1 + 0)
m, n: nat
IHm: binary m + binary n.+1 = binary (m + n.+1)
IHn: binary m + binary n = binary (m + n) ->
binary m.+1 + binary n = binary (m.+1 + n)
binary m.+1 + binary n.+1 = binary (m.+1 + n.+1)
    -
m: nat
IHm: binary m + binary 0 = binary (m + 0)
binary m.+1 + binary 0 = binary (m.+1 + 0) simpl.
m: nat
IHm: binary m + binary 0 = binary (m + 0)
Succ (binary m) + bzero = Succ (binary (m + 0)) rewrite binnatplussucc.
m: nat
IHm: binary m + binary 0 = binary (m + 0)
Succ (binary m + bzero) = Succ (binary (m + 0)) apply ap.
m: nat
IHm: binary m + binary 0 = binary (m + 0)
binary m + bzero = binary (m + 0) done.
    -
m, n: nat
IHm: binary m + binary n.+1 = binary (m + n.+1)
IHn: binary m + binary n = binary (m + n) ->
binary m.+1 + binary n = binary (m.+1 + n)
binary m.+1 + binary n.+1 = binary (m.+1 + n.+1) simpl.
m, n: nat
IHm: binary m + binary n.+1 = binary (m + n.+1)
IHn: binary m + binary n = binary (m + n) ->
binary m.+1 + binary n = binary (m.+1 + n)
Succ (binary m) + Succ (binary n) =
Succ (binary (m + n.+1)) rewrite <- IHm.
m, n: nat
IHm: binary m + binary n.+1 = binary (m + n.+1)
IHn: binary m + binary n = binary (m + n) ->
binary m.+1 + binary n = binary (m.+1 + n)
Succ (binary m) + Succ (binary n) =
Succ (binary m + binary n.+1) rewrite binnatplussucc.
m, n: nat
IHm: binary m + binary n.+1 = binary (m + n.+1)
IHn: binary m + binary n = binary (m + n) ->
binary m.+1 + binary n = binary (m.+1 + n)
Succ (binary m + Succ (binary n)) =
Succ (binary m + binary n.+1) done.
  Qed.

  Definition unaryplus (m n : binnat) : unary m + unary n = unary (m + n).
m, n: binnat
binary^-1 m + binary^-1 n = binary^-1 (m + n)
  Proof.
m, n: binnat
binary^-1 m + binary^-1 n = binary^-1 (m + n)
    etransitivity (unary (binary (_^-1 m + _^-1 n))).
m, n: binnat
binary^-1 m + binary^-1 n =
equiv_binary^-1 (binary (?f^-1 m + ?f0^-1 n))
m, n: binnat
equiv_binary^-1 (binary (?f^-1 m + ?f0^-1 n)) =
binary^-1 (m + n)
    -
m, n: binnat
binary^-1 m + binary^-1 n =
equiv_binary^-1 (binary (?f^-1 m + ?f0^-1 n)) apply ((eissect binary (unary m + unary n)) ^).
    -
m, n: binnat
binary^-1 (binary (binary^-1 m + binary^-1 n)) =
binary^-1 (m + n) rewrite <- binaryplus.
m, n: binnat
binary^-1
  (binary (binary^-1 m) + binary (binary^-1 n)) =
binary^-1 (m + n)
      rewrite (eisretr binary m), (eisretr binary n).
m, n: binnat
binary^-1 (m + n) = binary^-1 (m + n)
      reflexivity.
  Qed.

  Local Instance binnat_add_assoc : Associative binnat_plus.
Associative binnat_plus
  Proof.
Associative binnat_plus
    hnf; equiv_intros binary x y z.
x, y, z: nat
binnat_plus (binary x)
  (binnat_plus (binary y) (binary z)) =
binnat_plus (binnat_plus (binary x) (binary y))
  (binary z)
    change binnat_plus with plus.
x, y, z: nat
binary x + (binary y + binary z) =
binary x + binary y + binary z
    rewrite binaryplus, binaryplus, binaryplus, binaryplus.
x, y, z: nat
binary (x + (y + z)) = binary (x + y + z)
    apply ap.
x, y, z: nat
(x + (y + z))%nat = (x + y + z)%nat
    apply associativity.
  Qed.

  Local Instance binnat_add_comm : Commutative binnat_plus.
Commutative binnat_plus
  Proof.
Commutative binnat_plus
    hnf; equiv_intros binary x y.
x, y: nat
binnat_plus (binary x) (binary y) =
binnat_plus (binary y) (binary x)
    change binnat_plus with plus.
x, y: nat
binary x + binary y = binary y + binary x
    rewrite binaryplus, binaryplus.
x, y: nat
binary (x + y) = binary (y + x)
    apply ap.
x, y: nat
(x + y)%nat = (y + x)%nat
    apply plus_comm.
  Qed.

  Definition binnatmultsucc : forall (m n : binnat), (Succ m) * n = n + (m * n).
forall m n : binnat, Succ m * n = n + m * n
  Proof.
forall m n : binnat, Succ m * n = n + m * n
    induction m.
forall n : binnat, Succ bzero * n = n + bzero * n
m: binnat
IHm: forall n : binnat, Succ m * n = n + m * n
forall n : binnat,
Succ (double1 m) * n = n + double1 m * n
m: binnat
IHm: forall n : binnat, Succ m * n = n + m * n
forall n : binnat,
Succ (double2 m) * n = n + double2 m * n
    -
forall n : binnat, Succ bzero * n = n + bzero * n intros n.
n: binnat
Succ bzero * n = n + bzero * n change (bzero + n = n + bzero).
n: binnat
bzero + n = n + bzero
      apply commutativity.
    -
m: binnat
IHm: forall n : binnat, Succ m * n = n + m * n
forall n : binnat,
Succ (double1 m) * n = n + double1 m * n intros n.
m: binnat
IHm: forall n : binnat, Succ m * n = n + m * n
n: binnat
Succ (double1 m) * n = n + double1 m * n simpl.
m: binnat
IHm: forall n : binnat, Succ m * n = n + m * n
n: binnat
double2 m * n = n + double1 m * n
      change (double2 m * n) with ((m * n) + (m * n) + n + n).
m: binnat
IHm: forall n : binnat, Succ m * n = n + m * n
n: binnat
m * n + m * n + n + n = n + double1 m * n
      apply commutativity.
    -
m: binnat
IHm: forall n : binnat, Succ m * n = n + m * n
forall n : binnat,
Succ (double2 m) * n = n + double2 m * n intros n.
m: binnat
IHm: forall n : binnat, Succ m * n = n + m * n
n: binnat
Succ (double2 m) * n = n + double2 m * n simpl.
m: binnat
IHm: forall n : binnat, Succ m * n = n + m * n
n: binnat
double1 (Succ m) * n = n + double2 m * n
      change (double1 (Succ m) * n) with ((Succ m) * n + (Succ m) * n + n).
m: binnat
IHm: forall n : binnat, Succ m * n = n + m * n
n: binnat
Succ m * n + Succ m * n + n = n + double2 m * n
      rewrite IHm.
m: binnat
IHm: forall n : binnat, Succ m * n = n + m * n
n: binnat
n + m * n + (n + m * n) + n = n + double2 m * n
      rewrite (commutativity n (double2 m * n)).
m: binnat
IHm: forall n : binnat, Succ m * n = n + m * n
n: binnat
n + m * n + (n + m * n) + n = double2 m * n + n
      rewrite (commutativity n (m * n)).
m: binnat
IHm: forall n : binnat, Succ m * n = n + m * n
n: binnat
m * n + n + (m * n + n) + n = double2 m * n + n
      rewrite <- (associativity (m * n) n (m * n + n)).
m: binnat
IHm: forall n : binnat, Succ m * n = n + m * n
n: binnat
m * n + (n + (m * n + n)) + n = double2 m * n + n
      rewrite (commutativity n (m * n + n)).
m: binnat
IHm: forall n : binnat, Succ m * n = n + m * n
n: binnat
m * n + (m * n + n + n) + n = double2 m * n + n
      rewrite (associativity (m * n) _ _).
m: binnat
IHm: forall n : binnat, Succ m * n = n + m * n
n: binnat
m * n + (m * n + n) + n + n = double2 m * n + n
      rewrite (associativity (m * n) (m * n) n).
m: binnat
IHm: forall n : binnat, Succ m * n = n + m * n
n: binnat
m * n + m * n + n + n + n = double2 m * n + n
      done.
  Qed.

  Definition binarymult (m n : nat) : binary m * binary n = binary (m * n).
m, n: nat
binary m * binary n = binary (m * n)
  Proof.
m, n: nat
binary m * binary n = binary (m * n)
    induction m; induction n; try reflexivity; rewrite binnatmultsucc, IHm, binaryplus; done.
  Qed.

  Definition unarymult (m n : binnat) : unary m * unary n = unary (m * n).
m, n: binnat
binary^-1 m * binary^-1 n = binary^-1 (m * n)
  Proof.
m, n: binnat
binary^-1 m * binary^-1 n = binary^-1 (m * n)
    etransitivity (unary (binary (_^-1 m * _^-1 n))).
m, n: binnat
binary^-1 m * binary^-1 n =
equiv_binary^-1 (binary (?f^-1 m * ?f0^-1 n))
m, n: binnat
equiv_binary^-1 (binary (?f^-1 m * ?f0^-1 n)) =
binary^-1 (m * n)
    -
m, n: binnat
binary^-1 m * binary^-1 n =
equiv_binary^-1 (binary (?f^-1 m * ?f0^-1 n)) apply ((eissect binary (unary m * unary n)) ^).
    -
m, n: binnat
binary^-1 (binary (binary^-1 m * binary^-1 n)) =
binary^-1 (m * n) rewrite <- binarymult.
m, n: binnat
binary^-1
  (binary (binary^-1 m) * binary (binary^-1 n)) =
binary^-1 (m * n)
      rewrite (eisretr binary m), (eisretr binary n).
m, n: binnat
binary^-1 (m * n) = binary^-1 (m * n)
      reflexivity.
  Qed.

  Local Instance binnat_mult_assoc : Associative binnat_mult.
Associative binnat_mult
  Proof.
Associative binnat_mult
    hnf; equiv_intros binary x y z.
x, y, z: nat
binnat_mult (binary x)
  (binnat_mult (binary y) (binary z)) =
binnat_mult (binnat_mult (binary x) (binary y))
  (binary z)
    change binnat_mult with mult.
x, y, z: nat
binary x * (binary y * binary z) =
binary x * binary y * binary z
    rewrite binarymult, binarymult, binarymult, binarymult.
x, y, z: nat
binary (x * (y * z)) = binary (x * y * z)
    apply ap.
x, y, z: nat
(x * (y * z))%nat = (x * y * z)%nat
    apply associativity.
  Qed.

  Local Instance binnat_mult_comm : Commutative binnat_mult.
Commutative binnat_mult
  Proof.
Commutative binnat_mult
    hnf; equiv_intros binary x y.
x, y: nat
binnat_mult (binary x) (binary y) =
binnat_mult (binary y) (binary x)
    change binnat_mult with mult.
x, y: nat
binary x * binary y = binary y * binary x
    rewrite binarymult, binarymult.
x, y: nat
binary (x * y) = binary (y * x)
    apply ap.
x, y: nat
(x * y)%nat = (y * x)%nat
    apply commutativity.
  Qed.

  Local Instance binnat_distr_l : LeftDistribute binnat_mult binnat_plus.
LeftDistribute binnat_mult binnat_plus
  Proof.
LeftDistribute binnat_mult binnat_plus
    hnf; equiv_intros binary x y z.
x, y, z: nat
binnat_mult (binary x)
  (binnat_plus (binary y) (binary z)) =
binnat_plus (binnat_mult (binary x) (binary y))
  (binnat_mult (binary x) (binary z))
    change binnat_plus with plus.
x, y, z: nat
binnat_mult (binary x) (binary y + binary z) =
binnat_mult (binary x) (binary y) +
binnat_mult (binary x) (binary z)
    change binnat_mult with mult.
x, y, z: nat
binary x * (binary y + binary z) =
binary x * binary y + binary x * binary z
    rewrite binaryplus, binarymult, binarymult, binarymult, binaryplus.
x, y, z: nat
binary (x * (y + z)) = binary (x * y + x * z)
    apply ap.
x, y, z: nat
(x * (y + z))%nat = (x * y + x * z)%nat
    apply plus_mult_distr_l.
  Qed.

  Local Instance binnat_distr_r : RightDistribute binnat_mult binnat_plus.
RightDistribute binnat_mult binnat_plus
  Proof.
RightDistribute binnat_mult binnat_plus
    hnf; equiv_intros binary x y z.
x, y, z: nat
binnat_mult (binnat_plus (binary x) (binary y))
  (binary z) =
binnat_plus (binnat_mult (binary x) (binary z))
  (binnat_mult (binary y) (binary z))
    change binnat_plus with plus.
x, y, z: nat
binnat_mult (binary x + binary y) (binary z) =
binnat_mult (binary x) (binary z) +
binnat_mult (binary y) (binary z)
    change binnat_mult with mult.
x, y, z: nat
(binary x + binary y) * binary z =
binary x * binary z + binary y * binary z
    rewrite binaryplus, binarymult, binarymult, binarymult, binaryplus.
x, y, z: nat
binary ((x + y) * z) = binary (x * z + y * z)
    apply ap.
x, y, z: nat
((x + y) * z)%nat = (x * z + y * z)%nat
    apply plus_mult_distr_r.
  Qed.

  #[export] Instance binnat_set : IsHSet binnat.
IsHSet binnat
  Proof.
IsHSet binnat
    apply (istrunc_isequiv_istrunc nat binary).
  Qed.

  #[export] Instance binnat_semiring : IsSemiCRing binnat.
IsSemiCRing binnat
  Proof.
IsSemiCRing binnat
    split; try split; try split; try split; hnf; intros.
IsHSet binnat
x, y, z: binnat
sg_op x (sg_op y z) = sg_op (sg_op x y) z
x: binnat
sg_op x mon_unit = x
x, y: binnat
sg_op x y = sg_op y x
IsHSet binnat
x, y, z: binnat
sg_op x (sg_op y z) = sg_op (sg_op x y) z
x: binnat
sg_op x mon_unit = x
x, y: binnat
sg_op x y = sg_op y x
a, b, c: binnat
a * (b + c) = a * b + a * c
    1, 5: apply istrunc_S; intros x y; exact (binnat_set x y).
x, y, z: binnat
sg_op x (sg_op y z) = sg_op (sg_op x y) z
x: binnat
sg_op x mon_unit = x
x, y: binnat
sg_op x y = sg_op y x
x, y, z: binnat
sg_op x (sg_op y z) = sg_op (sg_op x y) z
x: binnat
sg_op x mon_unit = x
x, y: binnat
sg_op x y = sg_op y x
a, b, c: binnat
a * (b + c) = a * b + a * c
    all: apply (equiv_inj unary).
x, y, z: binnat
binary^-1 (sg_op x (sg_op y z)) =
binary^-1 (sg_op (sg_op x y) z)
x: binnat
binary^-1 (sg_op x mon_unit) = binary^-1 x
x, y: binnat
binary^-1 (sg_op x y) = binary^-1 (sg_op y x)
x, y, z: binnat
binary^-1 (sg_op x (sg_op y z)) =
binary^-1 (sg_op (sg_op x y) z)
x: binnat
binary^-1 (sg_op x mon_unit) = binary^-1 x
x, y: binnat
binary^-1 (sg_op x y) = binary^-1 (sg_op y x)
a, b, c: binnat
binary^-1 (a * (b + c)) = binary^-1 (a * b + a * c)
    1, 2, 3, 7: repeat rewrite <- unaryplus.
x, y, z: binnat
binary^-1 x + (binary^-1 y + binary^-1 z) =
binary^-1 x + binary^-1 y + binary^-1 z
x: binnat
binary^-1 x + binary^-1 mon_unit = binary^-1 x
x, y: binnat
binary^-1 x + binary^-1 y = binary^-1 y + binary^-1 x
a, b, c: binnat
binary^-1 (a * (b + c)) =
binary^-1 (a * b) + binary^-1 (a * c)
x, y, z: binnat
binary^-1 (sg_op x (sg_op y z)) =
binary^-1 (sg_op (sg_op x y) z)
x: binnat
binary^-1 (sg_op x mon_unit) = binary^-1 x
x, y: binnat
binary^-1 (sg_op x y) = binary^-1 (sg_op y x)
    4, 5, 6, 7: rewrite <- unarymult.
x, y, z: binnat
binary^-1 x + (binary^-1 y + binary^-1 z) =
binary^-1 x + binary^-1 y + binary^-1 z
x: binnat
binary^-1 x + binary^-1 mon_unit = binary^-1 x
x, y: binnat
binary^-1 x + binary^-1 y = binary^-1 y + binary^-1 x
a, b, c: binnat
binary^-1 a * binary^-1 (b + c) =
binary^-1 (a * b) + binary^-1 (a * c)
x, y, z: binnat
binary^-1 x * binary^-1 (sg_op y z) =
binary^-1 (sg_op (sg_op x y) z)
x: binnat
binary^-1 x * binary^-1 mon_unit = binary^-1 x
x, y: binnat
binary^-1 x * binary^-1 y = binary^-1 (sg_op y x)
    4, 5, 7: rewrite <- unarymult.
x, y, z: binnat
binary^-1 x + (binary^-1 y + binary^-1 z) =
binary^-1 x + binary^-1 y + binary^-1 z
x: binnat
binary^-1 x + binary^-1 mon_unit = binary^-1 x
x, y: binnat
binary^-1 x + binary^-1 y = binary^-1 y + binary^-1 x
a, b, c: binnat
binary^-1 a * binary^-1 (b + c) =
binary^-1 a * binary^-1 b + binary^-1 (a * c)
x, y, z: binnat
binary^-1 x * (binary^-1 y * binary^-1 z) =
binary^-1 (sg_op (sg_op x y) z)
x, y: binnat
binary^-1 x * binary^-1 y = binary^-1 y * binary^-1 x
x: binnat
binary^-1 x * binary^-1 mon_unit = binary^-1 x
    4, 5: rewrite <- unarymult.
x, y, z: binnat
binary^-1 x + (binary^-1 y + binary^-1 z) =
binary^-1 x + binary^-1 y + binary^-1 z
x: binnat
binary^-1 x + binary^-1 mon_unit = binary^-1 x
x, y: binnat
binary^-1 x + binary^-1 y = binary^-1 y + binary^-1 x
a, b, c: binnat
binary^-1 a * binary^-1 (b + c) =
binary^-1 a * binary^-1 b + binary^-1 a * binary^-1 c
x, y, z: binnat
binary^-1 x * (binary^-1 y * binary^-1 z) =
binary^-1 (sg_op x y) * binary^-1 z
x, y: binnat
binary^-1 x * binary^-1 y = binary^-1 y * binary^-1 x
x: binnat
binary^-1 x * binary^-1 mon_unit = binary^-1 x
    4: rewrite <- unaryplus.
x, y, z: binnat
binary^-1 x + (binary^-1 y + binary^-1 z) =
binary^-1 x + binary^-1 y + binary^-1 z
x: binnat
binary^-1 x + binary^-1 mon_unit = binary^-1 x
x, y: binnat
binary^-1 x + binary^-1 y = binary^-1 y + binary^-1 x
a, b, c: binnat
binary^-1 a * (binary^-1 b + binary^-1 c) =
binary^-1 a * binary^-1 b + binary^-1 a * binary^-1 c
x, y, z: binnat
binary^-1 x * (binary^-1 y * binary^-1 z) =
binary^-1 (sg_op x y) * binary^-1 z
x, y: binnat
binary^-1 x * binary^-1 y = binary^-1 y * binary^-1 x
x: binnat
binary^-1 x * binary^-1 mon_unit = binary^-1 x
    5: rewrite <- unarymult.
x, y, z: binnat
binary^-1 x + (binary^-1 y + binary^-1 z) =
binary^-1 x + binary^-1 y + binary^-1 z
x: binnat
binary^-1 x + binary^-1 mon_unit = binary^-1 x
x, y: binnat
binary^-1 x + binary^-1 y = binary^-1 y + binary^-1 x
a, b, c: binnat
binary^-1 a * (binary^-1 b + binary^-1 c) =
binary^-1 a * binary^-1 b + binary^-1 a * binary^-1 c
x, y, z: binnat
binary^-1 x * (binary^-1 y * binary^-1 z) =
binary^-1 x * binary^-1 y * binary^-1 z
x, y: binnat
binary^-1 x * binary^-1 y = binary^-1 y * binary^-1 x
x: binnat
binary^-1 x * binary^-1 mon_unit = binary^-1 x
    all: apply nat_semiring.
  Qed.

End semiring_laws.

Section naturals.

  Local Instance binary_preserving : IsSemiRingPreserving binary.
IsSemiRingPreserving binary
  Proof.
IsSemiRingPreserving binary
    split; split.
IsSemiGroupPreserving binary
IsUnitPreserving binary
IsSemiGroupPreserving binary
IsUnitPreserving binary
    1, 3: hnf; intros x y; [> apply (binaryplus x y) ^ | apply (binarymult x y) ^ ].
IsUnitPreserving binary
IsUnitPreserving binary
    all: reflexivity.
  Qed.

  #[export] Instance binnat_le : Le binnat := fun m n => unary m <= unary n.
  #[export] Instance binnat_lt : Lt binnat := fun m n => unary m < unary n.
  #[export] Instance binnat_apart : Apart binnat := fun m n => unary m ≶ unary n.
  Local Instance binnart_apart_symmetric : IsApart binnat.
IsApart binnat
  Proof.
IsApart binnat
    split.
IsHSet binnat
is_mere_relation binnat apart
Symmetric apart
CoTransitive apart
forall x y : binnat, ~ (x ≶ y) <-> x = y
    -
IsHSet binnat apply _.
    -
is_mere_relation binnat apart intros x y.
x, y: binnat
IsHProp (x ≶ y) apply nat_full.
    -
Symmetric apart intros x y.
x, y: binnat
x ≶ y -> y ≶ x apply nat_full.
    -
CoTransitive apart intros x y z w.
x, y: binnat
z: x ≶ y
w: binnat
hor (x ≶ w) (w ≶ y) apply nat_full.
x, y: binnat
z: x ≶ y
w: binnat
binary^-1 x ≶ binary^-1 y assumption.
    -
forall x y : binnat, ~ (x ≶ y) <-> x = y intros m n.
m, n: binnat
~ (m ≶ n) <-> m = n split.
m, n: binnat
~ (m ≶ n) -> m = n
m, n: binnat
m = n -> ~ (m ≶ n)
      +
m, n: binnat
~ (m ≶ n) -> m = n intros E.
m, n: binnat
E: ~ (m ≶ n)
m = n apply (equiv_inj unary).
m, n: binnat
E: ~ (m ≶ n)
binary^-1 m = binary^-1 n apply nat_full.
m, n: binnat
E: ~ (m ≶ n)
~ (binary^-1 m ≶ binary^-1 n) assumption.
      +
m, n: binnat
m = n -> ~ (m ≶ n) intros p.
m, n: binnat
p: m = n
~ (m ≶ n) apply nat_full.
m, n: binnat
p: m = n
binary^-1 m = binary^-1 n exact (ap unary p).
  Qed.

  Local Instance binnat_full : FullPseudoSemiRingOrder binnat_le binnat_lt.
FullPseudoSemiRingOrder binnat_le binnat_lt
  Proof.
FullPseudoSemiRingOrder binnat_le binnat_lt
    split.
is_mere_relation binnat binnat_le
PseudoSemiRingOrder binnat_lt
forall x y : binnat, x ≤ y <-> ~ (y < x)
    -
is_mere_relation binnat binnat_le intros m n; apply nat_le_hprop.
    -
PseudoSemiRingOrder binnat_lt split; try intros m n; try apply nat_full.
PseudoOrder binnat_lt
m, n: binnat
~ (n < m) -> {z : binnat & n = m + z}
forall z : binnat, StrictOrderEmbedding (plus z)
m, n: binnat
forall x₂ y₂ : binnat,
m * n ≶ x₂ * y₂ -> hor (m ≶ x₂) (n ≶ y₂)
m, n: binnat
PropHolds (0 < m) ->
PropHolds (0 < n) -> PropHolds (0 < m * n)
      +
PseudoOrder binnat_lt split; try intros m n; try apply nat_full.
IsApart binnat
m, n: binnat
m < n -> forall z : binnat, hor (m < z) (z < n)
        *
IsApart binnat split; try intros m n; try apply nat_full.
IsHSet binnat
m, n: binnat
m ≶ n -> forall z : binnat, hor (m ≶ z) (z ≶ n)
m, n: binnat
~ (m ≶ n) <-> m = n
          --
IsHSet binnat apply _.
          --
m, n: binnat
m ≶ n -> forall z : binnat, hor (m ≶ z) (z ≶ n) apply cotransitive.
          --
m, n: binnat
~ (m ≶ n) <-> m = n split; intros E.
m, n: binnat
E: ~ (m ≶ n)
m = n
m, n: binnat
E: m = n
~ (m ≶ n)
             ++
m, n: binnat
E: ~ (m ≶ n)
m = n assert (X : unary m = unary n) by by apply tight_apart.
m, n: binnat
E: ~ (m ≶ n)
X: binary^-1 m = binary^-1 n
m = n
                apply (((equiv_ap unary m n) ^-1) X).
             ++
m, n: binnat
E: m = n
~ (m ≶ n) rewrite E.
m, n: binnat
E: m = n
~ (n ≶ n) apply nat_full.
m, n: binnat
E: m = n
binary^-1 n = binary^-1 n reflexivity.
        *
m, n: binnat
m < n -> forall z : binnat, hor (m < z) (z < n) intros E k.
m, n: binnat
E: m < n
k: binnat
hor (m < k) (k < n) apply nat_full.
m, n: binnat
E: m < n
k: binnat
binary^-1 m < binary^-1 n exact E.
      +
m, n: binnat
~ (n < m) -> {z : binnat & n = m + z} intros E.
m, n: binnat
E: ~ (n < m)
{z : binnat & n = m + z}
        assert (H : exists w, (unary n) = (unary m) + w) by by apply nat_full.
m, n: binnat
E: ~ (n < m)
H: {w : nat & binary^-1 n = binary^-1 m + w}
{z : binnat & n = m + z}
        destruct H as [w L].
m, n: binnat
E: ~ (n < m)
w: nat
L: binary^-1 n = binary^-1 m + w
{z : binnat & n = m + z}
        exists (binary w).
m, n: binnat
E: ~ (n < m)
w: nat
L: binary^-1 n = binary^-1 m + w
n = m + binary w
        rewrite <- (eisretr unary w), unaryplus in L.
m, n: binnat
E: ~ (n < m)
w: nat
L: binary^-1 n = binary^-1 (m + (binary^-1)^-1 w)
n = m + binary w
        apply (equiv_inj unary).
m, n: binnat
E: ~ (n < m)
w: nat
L: binary^-1 n = binary^-1 (m + (binary^-1)^-1 w)
binary^-1 n = binary^-1 (m + binary w) exact L.
      +
forall z : binnat, StrictOrderEmbedding (plus z) intros m.
m: binnat
StrictOrderEmbedding (plus m) split; intros k l E; unfold lt, binnat_lt in *.
m, k, l: binnat
E: binary^-1 k < binary^-1 l
binary^-1 (m + k) < binary^-1 (m + l)
m, k, l: binnat
E: binary^-1 (m + k) < binary^-1 (m + l)
binary^-1 k < binary^-1 l
        *
m, k, l: binnat
E: binary^-1 k < binary^-1 l
binary^-1 (m + k) < binary^-1 (m + l) rewrite <- unaryplus, <- unaryplus.
m, k, l: binnat
E: binary^-1 k < binary^-1 l
binary^-1 m + binary^-1 k < binary^-1 m + binary^-1 l apply nat_full.
m, k, l: binnat
E: binary^-1 k < binary^-1 l
binary^-1 k < binary^-1 l exact E.
        *
m, k, l: binnat
E: binary^-1 (m + k) < binary^-1 (m + l)
binary^-1 k < binary^-1 l rewrite <- unaryplus, <- unaryplus in E.
m, k, l: binnat
E: binary^-1 m + binary^-1 k <
binary^-1 m + binary^-1 l
binary^-1 k < binary^-1 l
          apply (strictly_order_reflecting (plus (unary m))).
m, k, l: binnat
E: binary^-1 m + binary^-1 k <
binary^-1 m + binary^-1 l
binary^-1 m + binary^-1 k < binary^-1 m + binary^-1 l exact E.
      +
m, n: binnat
forall x₂ y₂ : binnat,
m * n ≶ x₂ * y₂ -> hor (m ≶ x₂) (n ≶ y₂) intros k l E.
m, n, k, l: binnat
E: m * n ≶ k * l
hor (m ≶ k) (n ≶ l) apply nat_full.
m, n, k, l: binnat
E: m * n ≶ k * l
binary^-1 m * binary^-1 n ≶ binary^-1 k * binary^-1 l
        unfold apart, binnat_apart in E.
m, n, k, l: binnat
E: binary^-1 (m * n) ≶ binary^-1 (k * l)
binary^-1 m * binary^-1 n ≶ binary^-1 k * binary^-1 l
        rewrite <- (unarymult m n), <- (unarymult k l) in E.
m, n, k, l: binnat
E: binary^-1 m * binary^-1 n
≶ binary^-1 k * binary^-1 l
binary^-1 m * binary^-1 n ≶ binary^-1 k * binary^-1 l exact E.
      +
m, n: binnat
PropHolds (0 < m) ->
PropHolds (0 < n) -> PropHolds (0 < m * n) intros E F.
m, n: binnat
E: PropHolds (0 < m)
F: PropHolds (0 < n)
PropHolds (0 < m * n) unfold lt, binnat_lt.
m, n: binnat
E: PropHolds (0 < m)
F: PropHolds (0 < n)
PropHolds (binary^-1 0 < binary^-1 (m * n)) rewrite <- (unarymult m n).
m, n: binnat
E: PropHolds (0 < m)
F: PropHolds (0 < n)
PropHolds (binary^-1 0 < binary^-1 m * binary^-1 n)
        apply nat_full; assumption.
    -
forall x y : binnat, x ≤ y <-> ~ (y < x) intros m n.
m, n: binnat
m ≤ n <-> ~ (n < m) apply nat_full.
  Qed.

  #[export] Instance binnat_naturals_to_semiring : NaturalsToSemiRing binnat:=
    fun _ _ _ _ _ _ => fix f (n: binnat) :=
      match n with
      | bzero => 0
      | double1 n' => 2 * (f n') + 1
      | double2 n' => 2 * (f n') + 2 end.

  Definition nat_to_semiring_helper : NaturalsToSemiRing nat :=
    fun _ _ _ _ _ _ => fix f (n: nat) :=
      match n with
      | 0%nat => 0
      | S n' => 1 + f n'
      end.

  Section for_another_semiring.
    Universe U.
    Context {R:Type} `{IsSemiCRing R}.

    Notation toR := (naturals_to_semiring binnat R).
    Notation toR_fromnat := (naturals_to_semiring nat R).
    Notation toR_vianat := (toR_fromnat ∘ unary).

    Definition f_suc (m : binnat) : toR (Succ m) = (toR m)+1.
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
m: binnat
toR (Succ m) = toR m + 1
    Proof.
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
m: binnat
toR (Succ m) = toR m + 1
      induction m.
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
toR (Succ bzero) = toR bzero + 1
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
m: binnat
IHm: toR (Succ m) = toR m + 1
toR (Succ (double1 m)) = toR (double1 m) + 1
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
m: binnat
IHm: toR (Succ m) = toR m + 1
toR (Succ (double2 m)) = toR (double2 m) + 1
      -
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
toR (Succ bzero) = toR bzero + 1 change (2 * 0 + 1 = 0 + 1).
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
2 * 0 + 1 = 0 + 1
        rewrite mult_comm.
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
0 * 2 + 1 = 0 + 1
        rewrite mult_0_l.
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
0 + 1 = 0 + 1
        done.
      -
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
m: binnat
IHm: toR (Succ m) = toR m + 1
toR (Succ (double1 m)) = toR (double1 m) + 1 change (2 * (toR m) + 2 = 2 * (toR m) + 1 + 1).
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
m: binnat
IHm: toR (Succ m) = toR m + 1
2 * toR m + 2 = 2 * toR m + 1 + 1
        apply plus_assoc.
      -
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
m: binnat
IHm: toR (Succ m) = toR m + 1
toR (Succ (double2 m)) = toR (double2 m) + 1 induction m as [|m _|m _].
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
IHm: toR (Succ bzero) = toR bzero + 1
toR (Succ (double2 bzero)) = toR (double2 bzero) + 1
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
m: binnat
IHm: toR (Succ (double1 m)) = toR (double1 m) + 1
toR (Succ (double2 (double1 m))) =
toR (double2 (double1 m)) + 1
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
m: binnat
IHm: toR (Succ (double2 m)) = toR (double2 m) + 1
toR (Succ (double2 (double2 m))) =
toR (double2 (double2 m)) + 1
        +
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
IHm: toR (Succ bzero) = toR bzero + 1
toR (Succ (double2 bzero)) = toR (double2 bzero) + 1 change (2 * (2 * 0 + 1) + 1 = 2 * 0 + 2 + 1).
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
IHm: toR (Succ bzero) = toR bzero + 1
2 * (2 * 0 + 1) + 1 = 2 * 0 + 2 + 1
          rewrite plus_mult_distr_l.
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
IHm: toR (Succ bzero) = toR bzero + 1
2 * (2 * 0) + 2 * 1 + 1 = 2 * 0 + 2 + 1
          rewrite (@mult_1_r _ Aplus Amult Azero Aone H _).
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
IHm: toR (Succ bzero) = toR bzero + 1
2 * (2 * 0) + 2 + 1 = 2 * 0 + 2 + 1
          rewrite mult_0_r, mult_0_r.
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
IHm: toR (Succ bzero) = toR bzero + 1
0 + 2 + 1 = 0 + 2 + 1
          reflexivity.
        +
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
m: binnat
IHm: toR (Succ (double1 m)) = toR (double1 m) + 1
toR (Succ (double2 (double1 m))) =
toR (double2 (double1 m)) + 1 change (2 * (2 * (toR m) + 2) + 1 = 2 * (2 * (toR m) + 1 ) + 2 + 1).
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
m: binnat
IHm: toR (Succ (double1 m)) = toR (double1 m) + 1
2 * (2 * toR m + 2) + 1 = 2 * (2 * toR m + 1) + 2 + 1
          apply (ap (fun z => z + 1)).
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
m: binnat
IHm: toR (Succ (double1 m)) = toR (double1 m) + 1
2 * (2 * toR m + 2) = 2 * (2 * toR m + 1) + 2
          assert (L : 2 * toR m + 2 = 2 * toR m + 1 + 1) by by rewrite plus_assoc.
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
m: binnat
IHm: toR (Succ (double1 m)) = toR (double1 m) + 1
L: 2 * toR m + 2 = 2 * toR m + 1 + 1
2 * (2 * toR m + 2) = 2 * (2 * toR m + 1) + 2
          rewrite L; clear L.
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
m: binnat
IHm: toR (Succ (double1 m)) = toR (double1 m) + 1
2 * (2 * toR m + 1 + 1) = 2 * (2 * toR m + 1) + 2
          rewrite plus_mult_distr_l.
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
m: binnat
IHm: toR (Succ (double1 m)) = toR (double1 m) + 1
2 * (2 * toR m + 1) + 2 * 1 = 2 * (2 * toR m + 1) + 2
          rewrite mult_1_r.
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
m: binnat
IHm: toR (Succ (double1 m)) = toR (double1 m) + 1
2 * (2 * toR m + 1) + 2 = 2 * (2 * toR m + 1) + 2
          reflexivity.
        +
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
m: binnat
IHm: toR (Succ (double2 m)) = toR (double2 m) + 1
toR (Succ (double2 (double2 m))) =
toR (double2 (double2 m)) + 1 simpl in IHm.
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
m: binnat
IHm: toR (double1 (Succ m)) = toR (double2 m) + 1
toR (Succ (double2 (double2 m))) =
toR (double2 (double2 m)) + 1
          change ((2 * (toR (double1 (Succ m))) + 1 = 2 * (toR (double2 m)) + 2 + 1)).
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
m: binnat
IHm: toR (double1 (Succ m)) = toR (double2 m) + 1
2 * toR (double1 (Succ m)) + 1 =
2 * toR (double2 m) + 2 + 1
          rewrite IHm; clear IHm.
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
m: binnat
2 * (toR (double2 m) + 1) + 1 =
2 * toR (double2 m) + 2 + 1
          rewrite plus_mult_distr_l.
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
m: binnat
2 * toR (double2 m) + 2 * 1 + 1 =
2 * toR (double2 m) + 2 + 1
          rewrite mult_1_r.
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
m: binnat
2 * toR (double2 m) + 2 + 1 =
2 * toR (double2 m) + 2 + 1
          reflexivity.
    Qed.

    Definition f_nat : forall m : binnat, toR m = toR_vianat m.
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
forall m : binnat, toR m = (toR_fromnat ∘ binary^-1) m
    Proof.
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
forall m : binnat, toR m = (toR_fromnat ∘ binary^-1) m
      equiv_intro binary n.
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
n: nat
toR (binary n) = (toR_fromnat ∘ binary^-1) (binary n)
      induction n as [|n IHn].
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
toR (binary 0) = (toR_fromnat ∘ binary^-1) (binary 0)
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
n: nat
IHn: toR (binary n) =
(toR_fromnat ∘ binary^-1) (binary n)
toR (binary n.+1) =
(toR_fromnat ∘ binary^-1) (binary n.+1)
      -
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
toR (binary 0) = (toR_fromnat ∘ binary^-1) (binary 0) reflexivity.
      -
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
n: nat
IHn: toR (binary n) =
(toR_fromnat ∘ binary^-1) (binary n)
toR (binary n.+1) =
(toR_fromnat ∘ binary^-1) (binary n.+1) induction n as [|n _].
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
IHn: toR (binary 0) =
(toR_fromnat ∘ binary^-1) (binary 0)
toR (binary 1) = (toR_fromnat ∘ binary^-1) (binary 1)
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
n: nat
IHn: toR (binary n.+1) =
(toR_fromnat ∘ binary^-1) (binary n.+1)
toR (binary n.+2) =
(toR_fromnat ∘ binary^-1) (binary n.+2)
        +
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
IHn: toR (binary 0) =
(toR_fromnat ∘ binary^-1) (binary 0)
toR (binary 1) = (toR_fromnat ∘ binary^-1) (binary 1) change ((1 + 1) * 0 + 1 = 1).
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
IHn: toR (binary 0) =
(toR_fromnat ∘ binary^-1) (binary 0)
2 * 0 + 1 = 1
          rewrite mult_0_r.
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
IHn: toR (binary 0) =
(toR_fromnat ∘ binary^-1) (binary 0)
0 + 1 = 1 apply plus_0_l.
        +
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
n: nat
IHn: toR (binary n.+1) =
(toR_fromnat ∘ binary^-1) (binary n.+1)
toR (binary n.+2) =
(toR_fromnat ∘ binary^-1) (binary n.+2) rewrite f_suc.
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
n: nat
IHn: toR (binary n.+1) =
(toR_fromnat ∘ binary^-1) (binary n.+1)
toR (Succ (nat_iter n Succ bzero)) + 1 =
(toR_fromnat ∘ binary^-1) (binary n.+2) rewrite IHn.
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
n: nat
IHn: toR (binary n.+1) =
(toR_fromnat ∘ binary^-1) (binary n.+1)
(toR_fromnat ∘ binary^-1) (binary n.+1) + 1 =
(toR_fromnat ∘ binary^-1) (binary n.+2)
          assert (L : (toR_fromnat ∘ binary^-1) (binary n.+1) + 1
                      = toR_fromnat ((binary^-1 (binary n.+1)).+1)%nat).
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
n: nat
IHn: toR (binary n.+1) =
(toR_fromnat ∘ binary^-1) (binary n.+1)
(toR_fromnat ∘ binary^-1) (binary n.+1) + 1 =
toR_fromnat (binary^-1 (binary n.+1)).+1%nat
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
n: nat
IHn: toR (binary n.+1) =
(toR_fromnat ∘ binary^-1) (binary n.+1)
L: (toR_fromnat ∘ binary^-1) (binary n.+1) + 1 =
toR_fromnat (binary^-1 (binary n.+1)).+1%nat
(toR_fromnat ∘ binary^-1) (binary n.+1) + 1 =
(toR_fromnat ∘ binary^-1) (binary n.+2)
          {
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
n: nat
IHn: toR (binary n.+1) =
(toR_fromnat ∘ binary^-1) (binary n.+1)
(toR_fromnat ∘ binary^-1) (binary n.+1) + 1 =
toR_fromnat (binary^-1 (binary n.+1)).+1%nat
            simpl rewrite (plus_comm _ 1).
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
n: nat
IHn: toR (binary n.+1) =
(toR_fromnat ∘ binary^-1) (binary n.+1)
1 + toR_fromnat (unary' (Succ (binary n))) =
match unary' (Succ (binary n)) with
| 0%nat => 1
| _.+1%nat =>
    1 + toR_fromnat (unary' (Succ (binary n)))
end
            simpl rewrite unarysucc.
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
n: nat
IHn: toR (binary n.+1) =
(toR_fromnat ∘ binary^-1) (binary n.+1)
1 + toR_fromnat (unary' (binary n)).+1%nat =
1 + toR_fromnat (unary' (binary n)).+1%nat
            reflexivity.
          }
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
n: nat
IHn: toR (binary n.+1) =
(toR_fromnat ∘ binary^-1) (binary n.+1)
L: (toR_fromnat ∘ binary^-1) (binary n.+1) + 1 =
toR_fromnat (binary^-1 (binary n.+1)).+1%nat
(toR_fromnat ∘ binary^-1) (binary n.+1) + 1 =
(toR_fromnat ∘ binary^-1) (binary n.+2)
          rewrite L; clear L.
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
n: nat
IHn: toR (binary n.+1) =
(toR_fromnat ∘ binary^-1) (binary n.+1)
toR_fromnat (binary^-1 (binary n.+1)).+1%nat =
(toR_fromnat ∘ binary^-1) (binary n.+2)
          rewrite <- unarysucc.
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
n: nat
IHn: toR (binary n.+1) =
(toR_fromnat ∘ binary^-1) (binary n.+1)
toR_fromnat (binary^-1 (Succ (binary n.+1))) =
(toR_fromnat ∘ binary^-1) (binary n.+2)
          rewrite <- binarysucc.
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
n: nat
IHn: toR (binary n.+1) =
(toR_fromnat ∘ binary^-1) (binary n.+1)
toR_fromnat (binary^-1 (binary n.+2)) =
(toR_fromnat ∘ binary^-1) (binary n.+2)
          reflexivity.
    Qed.

    Local Definition f_preserves_plus (a a' : binnat) : toR (a + a') = toR a + toR a'.
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
a, a': binnat
toR (a + a') = toR a + toR a'
    Proof.
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
a, a': binnat
toR (a + a') = toR a + toR a'
      rewrite f_nat, f_nat, f_nat.
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
a, a': binnat
(toR_fromnat ∘ binary^-1) (a + a') =
(toR_fromnat ∘ binary^-1) a +
(toR_fromnat ∘ binary^-1) a'
      unfold Compose.
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
a, a': binnat
toR_fromnat (binary^-1 (a + a')) =
toR_fromnat (binary^-1 a) + toR_fromnat (binary^-1 a')
      rewrite <- (unaryplus a a').
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
a, a': binnat
toR_fromnat (binary^-1 a + binary^-1 a') =
toR_fromnat (binary^-1 a) + toR_fromnat (binary^-1 a')
      apply nat_to_sr_morphism.
    Qed.

    Local Definition f_preserves_mult (a a' : binnat) : toR (a * a') = toR a * toR a'.
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
a, a': binnat
toR (a * a') = toR a * toR a'
    Proof.
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
a, a': binnat
toR (a * a') = toR a * toR a'
      rewrite f_nat, f_nat, f_nat.
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
a, a': binnat
(toR_fromnat ∘ binary^-1) (a * a') =
(toR_fromnat ∘ binary^-1) a *
(toR_fromnat ∘ binary^-1) a'
      unfold Compose.
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
a, a': binnat
toR_fromnat (binary^-1 (a * a')) =
toR_fromnat (binary^-1 a) * toR_fromnat (binary^-1 a')
      rewrite <- (unarymult a a').
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
a, a': binnat
toR_fromnat (binary^-1 a * binary^-1 a') =
toR_fromnat (binary^-1 a) * toR_fromnat (binary^-1 a')
      apply nat_to_sr_morphism.
    Qed.

    #[export] Instance binnat_to_sr_morphism
      : IsSemiRingPreserving toR.
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
IsSemiRingPreserving toR
    Proof.
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
IsSemiRingPreserving toR
      split; split.
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
IsSemiGroupPreserving toR
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
IsUnitPreserving toR
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
IsSemiGroupPreserving toR
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
IsUnitPreserving toR
      -
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
IsSemiGroupPreserving toR rapply f_preserves_plus.
      -
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
IsUnitPreserving toR reflexivity.
      -
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
IsSemiGroupPreserving toR rapply f_preserves_mult.
      -
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
IsUnitPreserving toR unfold IsUnitPreserving.
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
toR mon_unit = mon_unit
        apply f_nat.
    Defined.

    Lemma binnat_toR_unique (h : binnat -> R) `{!IsSemiRingPreserving h} : forall x,
        toR x = h x.
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
h: binnat -> R
IsSemiRingPreserving0: IsSemiRingPreserving h
forall x : binnat, toR x = h x
    Proof.
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
h: binnat -> R
IsSemiRingPreserving0: IsSemiRingPreserving h
forall x : binnat, toR x = h x
      equiv_intro binary n.
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
h: binnat -> R
IsSemiRingPreserving0: IsSemiRingPreserving h
n: nat
toR (binary n) = h (binary n)
      rewrite f_nat; unfold Compose.
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
h: binnat -> R
IsSemiRingPreserving0: IsSemiRingPreserving h
n: nat
toR_fromnat (binary^-1 (binary n)) = h (binary n)
      rewrite eissect.
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
h: binnat -> R
IsSemiRingPreserving0: IsSemiRingPreserving h
n: nat
toR_fromnat n = h (binary n)
      refine (toR_unique (h ∘ binary) n).
    Qed.
  End for_another_semiring.

  #[export] Instance binnat_naturals : Naturals binnat.
Naturals binnat
  Proof.
Naturals binnat
    split.
IsSemiCRing binnat
FullPseudoSemiRingOrder binnat_le binnat_lt
forall (B : Type) (Aplus0 : Plus B) (Amult0 : Mult B)
(Azero0 : Zero B) (Aone0 : One B) (H : IsSemiCRing B),
IsSemiRingPreserving (naturals_to_semiring binnat B)
forall (B : Type) (Aplus0 : Plus B) (Amult0 : Mult B)
(Azero0 : Zero B) (Aone0 : One B) (H : IsSemiCRing B)
(h : binnat -> B),
IsSemiRingPreserving h ->
forall x : binnat,
naturals_to_semiring binnat B x = h x
    -
IsSemiCRing binnat exact binnat_semiring.
    -
FullPseudoSemiRingOrder binnat_le binnat_lt exact binnat_full.
    -
forall (B : Type) (Aplus0 : Plus B) (Amult0 : Mult B)
(Azero0 : Zero B) (Aone0 : One B) (H : IsSemiCRing B),
IsSemiRingPreserving (naturals_to_semiring binnat B) intros.
B: Type
Aplus0: Plus B
Amult0: Mult B
Azero0: Zero B
Aone0: One B
H: IsSemiCRing B
IsSemiRingPreserving (naturals_to_semiring binnat B) apply binnat_to_sr_morphism.
    -
forall (B : Type) (Aplus0 : Plus B) (Amult0 : Mult B)
(Azero0 : Zero B) (Aone0 : One B) (H : IsSemiCRing B)
(h : binnat -> B),
IsSemiRingPreserving h ->
forall x : binnat,
naturals_to_semiring binnat B x = h x intros.
B: Type
Aplus0: Plus B
Amult0: Mult B
Azero0: Zero B
Aone0: One B
H: IsSemiCRing B
h: binnat -> B
IsSemiRingPreserving0: IsSemiRingPreserving h
x: binnat
naturals_to_semiring binnat B x = h x apply binnat_toR_unique.
B: Type
Aplus0: Plus B
Amult0: Mult B
Azero0: Zero B
Aone0: One B
H: IsSemiCRing B
h: binnat -> B
IsSemiRingPreserving0: IsSemiRingPreserving h
x: binnat
IsSemiRingPreserving h assumption.
  Qed.

End naturals.

Section decidable.

  Local Definition ineq_bzero_double1 n : bzero <> double1 n.
n: binnat
bzero <> double1 n
  Proof.
n: binnat
bzero <> double1 n
    intros p.
n: binnat
p: bzero = double1 n
Empty
    change ((fun x => match x with | double1 y => Unit | _ => Empty end) bzero).
n: binnat
p: bzero = double1 n
(fun x : binnat =>
 match x with
 | double1 _ => Unit
 | _ => Empty
 end) bzero
    rapply (@transport binnat).
n: binnat
p: bzero = double1 n
?Goal = bzero
n: binnat
p: bzero = double1 n
match ?Goal with
| double1 _ => Unit
| _ => Empty
end
    -
n: binnat
p: bzero = double1 n
?Goal = bzero exact p^.
    -
n: binnat
p: bzero = double1 n
match double1 n with
| double1 _ => Unit
| _ => Empty
end exact tt.
  Qed.

  Local Definition ineq_bzero_double2 n : bzero <> double2 n.
n: binnat
bzero <> double2 n
  Proof.
n: binnat
bzero <> double2 n
    intros p.
n: binnat
p: bzero = double2 n
Empty
    change ((fun x => match x with | double2 y => Unit | _ => Empty end) bzero).
n: binnat
p: bzero = double2 n
(fun x : binnat =>
 match x with
 | double2 _ => Unit
 | _ => Empty
 end) bzero
    rapply (@transport binnat).
n: binnat
p: bzero = double2 n
?Goal = bzero
n: binnat
p: bzero = double2 n
match ?Goal with
| double2 _ => Unit
| _ => Empty
end
    -
n: binnat
p: bzero = double2 n
?Goal = bzero exact p^.
    -
n: binnat
p: bzero = double2 n
match double2 n with
| double2 _ => Unit
| _ => Empty
end exact tt.
  Qed.

  Local Definition ineq_double1_double2 m n : double1 m <> double2 n.
m, n: binnat
double1 m <> double2 n
  Proof.
m, n: binnat
double1 m <> double2 n
    intros p.
m, n: binnat
p: double1 m = double2 n
Empty
    change ((fun x => match x with | double2 y => Unit | _ => Empty end) (double1 m)).
m, n: binnat
p: double1 m = double2 n
(fun x : binnat =>
 match x with
 | double2 _ => Unit
 | _ => Empty
 end) (double1 m)
    rapply (@transport binnat).
m, n: binnat
p: double1 m = double2 n
?Goal = double1 m
m, n: binnat
p: double1 m = double2 n
match ?Goal with
| double2 _ => Unit
| _ => Empty
end
    -
m, n: binnat
p: double1 m = double2 n
?Goal = double1 m exact p^.
    -
m, n: binnat
p: double1 m = double2 n
match double2 n with
| double2 _ => Unit
| _ => Empty
end exact tt.
  Qed.

  Local Definition undouble (m : binnat) : binnat :=
    match m with
    | bzero => bzero
    | double1 k => k
    | double2 k => k
    end.

  Local Instance double1_inj : IsInjective double1
  := { injective := fun a b E => ap undouble E }.

  Local Instance double2_inj : IsInjective double2
  := { injective := fun a b E => ap undouble E }.

  #[export] Instance binnat_dec : DecidablePaths binnat.
DecidablePaths binnat
  Proof.
DecidablePaths binnat
    intros m; induction m as [|m IHm|m IHm]; intros n; induction n as [|n IHn|n IHn].
Decidable (bzero = bzero)
n: binnat
IHn: Decidable (bzero = n)
Decidable (bzero = double1 n)
n: binnat
IHn: Decidable (bzero = n)
Decidable (bzero = double2 n)
m: binnat
IHm: forall y : binnat, Decidable (m = y)
Decidable (double1 m = bzero)
m: binnat
IHm: forall y : binnat, Decidable (m = y)
n: binnat
IHn: Decidable (double1 m = n)
Decidable (double1 m = double1 n)
m: binnat
IHm: forall y : binnat, Decidable (m = y)
n: binnat
IHn: Decidable (double1 m = n)
Decidable (double1 m = double2 n)
m: binnat
IHm: forall y : binnat, Decidable (m = y)
Decidable (double2 m = bzero)
m: binnat
IHm: forall y : binnat, Decidable (m = y)
n: binnat
IHn: Decidable (double2 m = n)
Decidable (double2 m = double1 n)
m: binnat
IHm: forall y : binnat, Decidable (m = y)
n: binnat
IHn: Decidable (double2 m = n)
Decidable (double2 m = double2 n)
    all:
      first
        [ left ; reflexivity
        | right ; (idtac + apply symmetric_neq);
          first
               [ apply ineq_bzero_double1
               | apply ineq_bzero_double2
               | apply ineq_double1_double2
               ]
        | destruct (IHm n) as [eq | ineq];
          [ left; apply ap; exact eq
          | right; intros E;
            first
              [ apply (injective double1) in E
              | apply (injective double2) in E
              ]; auto
          ]
        ].
  Defined.

End decidable.

Section other_laws.

Instance binnat_plus_cancel_l (z:binnat) : LeftCancellation plus z.
z: binnat
LeftCancellation plus z
Proof.
z: binnat
LeftCancellation plus z
  intros x y p.
z, x, y: binnat
p: z + x = z + y
x = y
  apply (equiv_inj unary).
z, x, y: binnat
p: z + x = z + y
binary^-1 x = binary^-1 y
  apply (ap unary) in p.
z, x, y: binnat
p: binary^-1 (z + x) = binary^-1 (z + y)
binary^-1 x = binary^-1 y
  rewrite <- unaryplus, <- unaryplus in p.
z, x, y: binnat
p: binary^-1 z + binary^-1 x =
binary^-1 z + binary^-1 y
binary^-1 x = binary^-1 y
  exact (left_cancellation _ _ _ _ p).
Qed.

Instance binnat_mult_cancel_l (z : binnat): PropHolds (z <> 0) -> LeftCancellation (.*.) z.
z: binnat
PropHolds (z <> 0) -> LeftCancellation mult z
Proof.
z: binnat
PropHolds (z <> 0) -> LeftCancellation mult z
  intros E.
z: binnat
E: PropHolds (z <> 0)
LeftCancellation mult z hnf in E.
z: binnat
E: z = 0 -> Empty
LeftCancellation mult z
  assert (H : unary z <> unary 0).
z: binnat
E: z = 0 -> Empty
binary^-1 z <> binary^-1 0
z: binnat
E: z = 0 -> Empty
H: binary^-1 z <> binary^-1 0
LeftCancellation mult z
  {
z: binnat
E: z = 0 -> Empty
binary^-1 z <> binary^-1 0
    intros q.
z: binnat
E: z = 0 -> Empty
q: binary^-1 z = binary^-1 0
Empty
    apply (equiv_inj unary) in q.
z: binnat
E: z = 0 -> Empty
q: z = 0
Empty
    exact (E q).
  }
z: binnat
E: z = 0 -> Empty
H: binary^-1 z <> binary^-1 0
LeftCancellation mult z
  intros x y p.
z: binnat
E: z = 0 -> Empty
H: binary^-1 z <> binary^-1 0
x, y: binnat
p: z * x = z * y
x = y
  apply (ap unary) in p.
z: binnat
E: z = 0 -> Empty
H: binary^-1 z <> binary^-1 0
x, y: binnat
p: binary^-1 (z * x) = binary^-1 (z * y)
x = y
  rewrite <- unarymult, <- unarymult in p.
z: binnat
E: z = 0 -> Empty
H: binary^-1 z <> binary^-1 0
x, y: binnat
p: binary^-1 z * binary^-1 x =
binary^-1 z * binary^-1 y
x = y
  exact (equiv_inj unary (nat_mult_cancel_l (unary z) H _ _ p)).
Qed.

Local Instance binnat_le_total : TotalRelation (_:Le binnat).
TotalRelation (binnat_le : Le binnat)
Proof.
TotalRelation (binnat_le : Le binnat)
  intros x y.
x, y: binnat
(binnat_le x y + binnat_le y x)%type apply nat_le_total.
Qed.
Local Instance binnat_lt_irrefl : Irreflexive (_:Lt binnat).
Irreflexive (binnat_lt : Lt binnat)
Proof.
Irreflexive (binnat_lt : Lt binnat)
  intros x.
x: binnat
complement binnat_lt x x apply nat_lt_irrefl.
Qed.

End other_laws.

Section trichotomy.

  (* TODO this is an inefficient implementation. Instead, write this
  without going via the unary naturals. *)
  Instance binnat_trichotomy : Trichotomy (lt:Lt binnat).
Trichotomy (lt : Lt binnat)
  Proof.
Trichotomy (lt : Lt binnat)
    intros x y.
x, y: binnat
((x < y) + ((x = y) + (y < x)))%type
    pose (T := nat_trichotomy (unary x) (unary y)).
x, y: binnat
T:= nat_trichotomy (binary^-1 x) (binary^-1 y): ((lt : Lt nat) (binary^-1 x) (binary^-1 y) +
 ((binary^-1 x = binary^-1 y) +
  (lt : Lt nat) (binary^-1 y) (binary^-1 x)))%type
((x < y) + ((x = y) + (y < x)))%type
    destruct T as [l|[c|r]].
x, y: binnat
l: binary^-1 x < binary^-1 y
((x < y) + ((x = y) + (y < x)))%type
x, y: binnat
c: binary^-1 x = binary^-1 y
((x < y) + ((x = y) + (y < x)))%type
x, y: binnat
r: binary^-1 y < binary^-1 x
((x < y) + ((x = y) + (y < x)))%type
    -
x, y: binnat
l: binary^-1 x < binary^-1 y
((x < y) + ((x = y) + (y < x)))%type left; assumption.
    -
x, y: binnat
c: binary^-1 x = binary^-1 y
((x < y) + ((x = y) + (y < x)))%type right; left.
x, y: binnat
c: binary^-1 x = binary^-1 y
x = y apply (equiv_inj unary); assumption.
    -
x, y: binnat
r: binary^-1 y < binary^-1 x
((x < y) + ((x = y) + (y < x)))%type right; right; assumption.
  Defined.

End trichotomy.

Section minus.

  Local Definition Pred (m : binnat) : binnat :=
    match m with
    | bzero      => bzero
    | double1 m' => double m'
    | double2 m' => double1 m'
    end.

  Local Definition succ_double (m : binnat) : Succ (double m) = double1 m.
m: binnat
Succ (double m) = double1 m
  Proof.
m: binnat
Succ (double m) = double1 m
    induction m.
Succ (double bzero) = double1 bzero
m: binnat
IHm: Succ (double m) = double1 m
Succ (double (double1 m)) = double1 (double1 m)
m: binnat
IHm: Succ (double m) = double1 m
Succ (double (double2 m)) = double1 (double2 m)
    -
Succ (double bzero) = double1 bzero reflexivity.
    -
m: binnat
IHm: Succ (double m) = double1 m
Succ (double (double1 m)) = double1 (double1 m) change (double1 (Succ (double m)) = double1 (double1 m)).
m: binnat
IHm: Succ (double m) = double1 m
double1 (Succ (double m)) = double1 (double1 m)
      rewrite IHm; reflexivity.
    -
m: binnat
IHm: Succ (double m) = double1 m
Succ (double (double2 m)) = double1 (double2 m) change (double1 (Succ (Succ (double m))) = double1 (double2 m)).
m: binnat
IHm: Succ (double m) = double1 m
double1 (Succ (Succ (double m))) = double1 (double2 m)
      rewrite IHm; reflexivity.
  Qed.

  Local Definition double_succ (m : binnat) : double (Succ m) = double2 m.
m: binnat
double (Succ m) = double2 m
  Proof.
m: binnat
double (Succ m) = double2 m
    induction m.
double (Succ bzero) = double2 bzero
m: binnat
IHm: double (Succ m) = double2 m
double (Succ (double1 m)) = double2 (double1 m)
m: binnat
IHm: double (Succ m) = double2 m
double (Succ (double2 m)) = double2 (double2 m)
    -
double (Succ bzero) = double2 bzero reflexivity.
    -
m: binnat
IHm: double (Succ m) = double2 m
double (Succ (double1 m)) = double2 (double1 m) change (double2 (Succ (double m)) = double2 (double1 m)).
m: binnat
IHm: double (Succ m) = double2 m
double2 (Succ (double m)) = double2 (double1 m)
      rewrite succ_double; reflexivity.
    -
m: binnat
IHm: double (Succ m) = double2 m
double (Succ (double2 m)) = double2 (double2 m) change (double2 (double (Succ m)) = double2 (double2 m)).
m: binnat
IHm: double (Succ m) = double2 m
double2 (double (Succ m)) = double2 (double2 m)
      rewrite IHm; reflexivity.
  Qed.

  Local Definition pred_succ (m : binnat) : Pred (Succ m) = m.
m: binnat
Pred (Succ m) = m
  Proof.
m: binnat
Pred (Succ m) = m
    induction m; try reflexivity.
m: binnat
IHm: Pred (Succ m) = m
Pred (Succ (double2 m)) = double2 m
    -
m: binnat
IHm: Pred (Succ m) = m
Pred (Succ (double2 m)) = double2 m exact (double_succ m).
  Qed.

  Local Definition double_pred (m : binnat) : double (Pred m) = Pred (Pred (double m)).
m: binnat
double (Pred m) = Pred (Pred (double m))
  Proof.
m: binnat
double (Pred m) = Pred (Pred (double m))
    induction m; try reflexivity.
m: binnat
IHm: double (Pred m) = Pred (Pred (double m))
double (Pred (double2 m)) =
Pred (Pred (double (double2 m)))
    -
m: binnat
IHm: double (Pred m) = Pred (Pred (double m))
double (Pred (double2 m)) =
Pred (Pred (double (double2 m))) exact (double_succ (double m))^.
  Qed.

  Local Definition pred_double2 (m : binnat) : Pred (double2 m) = double1 m.
m: binnat
Pred (double2 m) = double1 m
  Proof.
m: binnat
Pred (double2 m) = double1 m
    induction m; reflexivity.
  Qed.

  Local Definition pred_double1 (m : binnat) : Pred (double1 m) = double m.
m: binnat
Pred (double1 m) = double m
  Proof.
m: binnat
Pred (double1 m) = double m
    induction m; reflexivity.
  Qed.

  (*     2*(m-1)+1 = 2*m - 1 *)

  Local Fixpoint binnat_cut_minus' (m n : binnat) : binnat :=
    match m, n with
    | bzero      , n'         => bzero
    | m'         , bzero      => m'
    (* compute m - n as 2m'+1 - 2n'+1 = 2(m'-n') *)
    | double1 m' , double1 n' => double (binnat_cut_minus' m' n')
    (* compute m - n as 2m'+1 - 2n'+2 = 2(m'-n') - 1 = Pred (double (m' - n')) *)
    | double1 m' , double2 n' => Pred (double (binnat_cut_minus' m' n'))
    (* compute m - n as 2m'+2 - 2n'+1 *)
    | double2 m' , double1 n' => Pred (double (binnat_cut_minus' (Succ m') n'))
    (* compute m - n as 2m'+2 - 2n'+2 = 2(m'-n') = double (m' - n') *)
    | double2 m' , double2 n' => double (binnat_cut_minus' m' n')
    end.

  #[export] Instance binnat_cut_minus: CutMinus binnat := binnat_cut_minus'.

  Local Definition binnat_minus_zero (m : binnat) : m ∸ bzero = m.
m: binnat
m ∸ bzero = m
  Proof.
m: binnat
m ∸ bzero = m
    induction m; reflexivity.
  Qed.

  Local Definition binnat_zero_minus (m : binnat) : bzero ∸ m = bzero.
m: binnat
bzero ∸ m = bzero
  Proof.
m: binnat
bzero ∸ m = bzero
    induction m; reflexivity.
  Qed.

  Local Definition pred_succ_minus (m n : binnat) : Pred (Succ m ∸ n) = m ∸ n.
m, n: binnat
Pred (Succ m ∸ n) = m ∸ n
  Proof.
m, n: binnat
Pred (Succ m ∸ n) = m ∸ n
    revert n; induction m; intros n; induction n; try reflexivity.
n: binnat
IHn: Pred (Succ bzero ∸ n) = bzero ∸ n
Pred (Succ bzero ∸ double1 n) = bzero ∸ double1 n
n: binnat
IHn: Pred (Succ bzero ∸ n) = bzero ∸ n
Pred (Succ bzero ∸ double2 n) = bzero ∸ double2 n
m: binnat
IHm: forall n : binnat, Pred (Succ m ∸ n) = m ∸ n
n: binnat
IHn: Pred (Succ (double1 m) ∸ n) = double1 m ∸ n
Pred (Succ (double1 m) ∸ double1 n) =
double1 m ∸ double1 n
m: binnat
IHm: forall n : binnat, Pred (Succ m ∸ n) = m ∸ n
Pred (Succ (double2 m) ∸ bzero) = double2 m ∸ bzero
m: binnat
IHm: forall n : binnat, Pred (Succ m ∸ n) = m ∸ n
n: binnat
IHn: Pred (Succ (double2 m) ∸ n) = double2 m ∸ n
Pred (Succ (double2 m) ∸ double2 n) =
double2 m ∸ double2 n
    -
n: binnat
IHn: Pred (Succ bzero ∸ n) = bzero ∸ n
Pred (Succ bzero ∸ double1 n) = bzero ∸ double1 n change (Pred (double (bzero ∸ n)) = bzero).
n: binnat
IHn: Pred (Succ bzero ∸ n) = bzero ∸ n
Pred (double (bzero ∸ n)) = bzero
      rewrite binnat_zero_minus; reflexivity.
    -
n: binnat
IHn: Pred (Succ bzero ∸ n) = bzero ∸ n
Pred (Succ bzero ∸ double2 n) = bzero ∸ double2 n change (Pred (Pred (double (bzero ∸ n))) = bzero ∸ double2 n).
n: binnat
IHn: Pred (Succ bzero ∸ n) = bzero ∸ n
Pred (Pred (double (bzero ∸ n))) = bzero ∸ double2 n
      rewrite binnat_zero_minus, binnat_zero_minus; reflexivity.
    -
m: binnat
IHm: forall n : binnat, Pred (Succ m ∸ n) = m ∸ n
n: binnat
IHn: Pred (Succ (double1 m) ∸ n) = double1 m ∸ n
Pred (Succ (double1 m) ∸ double1 n) =
double1 m ∸ double1 n change (Pred (Pred (double (Succ m ∸ n))) = double (m ∸ n)).
m: binnat
IHm: forall n : binnat, Pred (Succ m ∸ n) = m ∸ n
n: binnat
IHn: Pred (Succ (double1 m) ∸ n) = double1 m ∸ n
Pred (Pred (double (Succ m ∸ n))) = double (m ∸ n)
      rewrite <- double_pred.
m: binnat
IHm: forall n : binnat, Pred (Succ m ∸ n) = m ∸ n
n: binnat
IHn: Pred (Succ (double1 m) ∸ n) = double1 m ∸ n
double (Pred (Succ m ∸ n)) = double (m ∸ n)
      apply ap.
m: binnat
IHm: forall n : binnat, Pred (Succ m ∸ n) = m ∸ n
n: binnat
IHn: Pred (Succ (double1 m) ∸ n) = double1 m ∸ n
Pred (Succ m ∸ n) = m ∸ n
      exact (IHm n).
    -
m: binnat
IHm: forall n : binnat, Pred (Succ m ∸ n) = m ∸ n
Pred (Succ (double2 m) ∸ bzero) = double2 m ∸ bzero change (double (Succ m) = double2 m ∸ bzero).
m: binnat
IHm: forall n : binnat, Pred (Succ m ∸ n) = m ∸ n
double (Succ m) = double2 m ∸ bzero
      rewrite binnat_minus_zero.
m: binnat
IHm: forall n : binnat, Pred (Succ m ∸ n) = m ∸ n
double (Succ m) = double2 m
      exact (double_succ m).
    -
m: binnat
IHm: forall n : binnat, Pred (Succ m ∸ n) = m ∸ n
n: binnat
IHn: Pred (Succ (double2 m) ∸ n) = double2 m ∸ n
Pred (Succ (double2 m) ∸ double2 n) =
double2 m ∸ double2 n change (Pred (Pred (double (Succ m ∸ n))) = double (m ∸ n)).
m: binnat
IHm: forall n : binnat, Pred (Succ m ∸ n) = m ∸ n
n: binnat
IHn: Pred (Succ (double2 m) ∸ n) = double2 m ∸ n
Pred (Pred (double (Succ m ∸ n))) = double (m ∸ n)
      rewrite <- double_pred.
m: binnat
IHm: forall n : binnat, Pred (Succ m ∸ n) = m ∸ n
n: binnat
IHn: Pred (Succ (double2 m) ∸ n) = double2 m ∸ n
double (Pred (Succ m ∸ n)) = double (m ∸ n)
      apply ap.
m: binnat
IHm: forall n : binnat, Pred (Succ m ∸ n) = m ∸ n
n: binnat
IHn: Pred (Succ (double2 m) ∸ n) = double2 m ∸ n
Pred (Succ m ∸ n) = m ∸ n
      exact (IHm n).
  Qed.

  Local Definition double_cases (m : binnat) : (bzero = double m) + hfiber double2 (double m).
m: binnat
((bzero = double m) + hfiber double2 (double m))%type
  Proof.
m: binnat
((bzero = double m) + hfiber double2 (double m))%type
    induction m.
((bzero = double bzero) +
 hfiber double2 (double bzero))%type
m: binnat
IHm: ((bzero = double m) + hfiber double2 (double m))%type
((bzero = double (double1 m)) +
 hfiber double2 (double (double1 m)))%type
m: binnat
IHm: ((bzero = double m) + hfiber double2 (double m))%type
((bzero = double (double2 m)) +
 hfiber double2 (double (double2 m)))%type
    -
((bzero = double bzero) +
 hfiber double2 (double bzero))%type left; reflexivity.
    -
m: binnat
IHm: ((bzero = double m) + hfiber double2 (double m))%type
((bzero = double (double1 m)) +
 hfiber double2 (double (double1 m)))%type right; exists (double m); reflexivity.
    -
m: binnat
IHm: ((bzero = double m) + hfiber double2 (double m))%type
((bzero = double (double2 m)) +
 hfiber double2 (double (double2 m)))%type right; exists (Succ (double m)); reflexivity.
  Defined.

  Local Definition binnat_minus_succ (m n : binnat) : Succ m ∸ Succ n = m ∸ n.
m, n: binnat
Succ m ∸ Succ n = m ∸ n
  Proof.
m, n: binnat
Succ m ∸ Succ n = m ∸ n
    revert n; induction m; intros n; induction n; try reflexivity.
n: binnat
IHn: Succ bzero ∸ Succ n = bzero ∸ n
Succ bzero ∸ Succ (double1 n) = bzero ∸ double1 n
n: binnat
IHn: Succ bzero ∸ Succ n = bzero ∸ n
Succ bzero ∸ Succ (double2 n) = bzero ∸ double2 n
m: binnat
IHm: forall n : binnat, Succ m ∸ Succ n = m ∸ n
Succ (double1 m) ∸ Succ bzero = double1 m ∸ bzero
m: binnat
IHm: forall n : binnat, Succ m ∸ Succ n = m ∸ n
n: binnat
IHn: Succ (double1 m) ∸ Succ n = double1 m ∸ n
Succ (double1 m) ∸ Succ (double2 n) =
double1 m ∸ double2 n
m: binnat
IHm: forall n : binnat, Succ m ∸ Succ n = m ∸ n
Succ (double2 m) ∸ Succ bzero = double2 m ∸ bzero
m: binnat
IHm: forall n : binnat, Succ m ∸ Succ n = m ∸ n
n: binnat
IHn: Succ (double2 m) ∸ Succ n = double2 m ∸ n
Succ (double2 m) ∸ Succ (double2 n) =
double2 m ∸ double2 n
    -
n: binnat
IHn: Succ bzero ∸ Succ n = bzero ∸ n
Succ bzero ∸ Succ (double1 n) = bzero ∸ double1 n change (Pred (double (bzero ∸ n)) = bzero ∸ double1 n).
n: binnat
IHn: Succ bzero ∸ Succ n = bzero ∸ n
Pred (double (bzero ∸ n)) = bzero ∸ double1 n
      rewrite binnat_zero_minus, binnat_zero_minus.
n: binnat
IHn: Succ bzero ∸ Succ n = bzero ∸ n
Pred (double bzero) = bzero reflexivity.
    -
n: binnat
IHn: Succ bzero ∸ Succ n = bzero ∸ n
Succ bzero ∸ Succ (double2 n) = bzero ∸ double2 n change (double (bzero ∸ (Succ n)) = bzero ∸ double2 n).
n: binnat
IHn: Succ bzero ∸ Succ n = bzero ∸ n
double (bzero ∸ Succ n) = bzero ∸ double2 n
      rewrite binnat_zero_minus, binnat_zero_minus.
n: binnat
IHn: Succ bzero ∸ Succ n = bzero ∸ n
double bzero = bzero reflexivity.
    -
m: binnat
IHm: forall n : binnat, Succ m ∸ Succ n = m ∸ n
Succ (double1 m) ∸ Succ bzero = double1 m ∸ bzero change (Pred (double (Succ m ∸ bzero)) = double1 m ∸ bzero).
m: binnat
IHm: forall n : binnat, Succ m ∸ Succ n = m ∸ n
Pred (double (Succ m ∸ bzero)) = double1 m ∸ bzero
      rewrite binnat_minus_zero, binnat_minus_zero.
m: binnat
IHm: forall n : binnat, Succ m ∸ Succ n = m ∸ n
Pred (double (Succ m)) = double1 m
      rewrite double_succ, pred_double2.
m: binnat
IHm: forall n : binnat, Succ m ∸ Succ n = m ∸ n
double1 m = double1 m reflexivity.
    -
m: binnat
IHm: forall n : binnat, Succ m ∸ Succ n = m ∸ n
n: binnat
IHn: Succ (double1 m) ∸ Succ n = double1 m ∸ n
Succ (double1 m) ∸ Succ (double2 n) =
double1 m ∸ double2 n change (Pred (double (Succ m ∸ Succ n)) = Pred (double (m ∸ n))).
m: binnat
IHm: forall n : binnat, Succ m ∸ Succ n = m ∸ n
n: binnat
IHn: Succ (double1 m) ∸ Succ n = double1 m ∸ n
Pred (double (Succ m ∸ Succ n)) =
Pred (double (m ∸ n))
      rewrite IHm.
m: binnat
IHm: forall n : binnat, Succ m ∸ Succ n = m ∸ n
n: binnat
IHn: Succ (double1 m) ∸ Succ n = double1 m ∸ n
Pred (double (m ∸ n)) = Pred (double (m ∸ n)) reflexivity.
    -
m: binnat
IHm: forall n : binnat, Succ m ∸ Succ n = m ∸ n
Succ (double2 m) ∸ Succ bzero = double2 m ∸ bzero change (double (Succ m ∸ bzero) = double2 m ∸ bzero).
m: binnat
IHm: forall n : binnat, Succ m ∸ Succ n = m ∸ n
double (Succ m ∸ bzero) = double2 m ∸ bzero
      rewrite binnat_minus_zero, binnat_minus_zero, double_succ.
m: binnat
IHm: forall n : binnat, Succ m ∸ Succ n = m ∸ n
double2 m = double2 m
      reflexivity.
    -
m: binnat
IHm: forall n : binnat, Succ m ∸ Succ n = m ∸ n
n: binnat
IHn: Succ (double2 m) ∸ Succ n = double2 m ∸ n
Succ (double2 m) ∸ Succ (double2 n) =
double2 m ∸ double2 n change (double (Succ m ∸ Succ n) = double (m ∸ n)).
m: binnat
IHm: forall n : binnat, Succ m ∸ Succ n = m ∸ n
n: binnat
IHn: Succ (double2 m) ∸ Succ n = double2 m ∸ n
double (Succ m ∸ Succ n) = double (m ∸ n)
      rewrite IHm.
m: binnat
IHm: forall n : binnat, Succ m ∸ Succ n = m ∸ n
n: binnat
IHn: Succ (double2 m) ∸ Succ n = double2 m ∸ n
double (m ∸ n) = double (m ∸ n) reflexivity.
  Qed.

  Local Definition binaryminus (x y : nat) : binary x ∸ binary y = binary (x ∸ y).
x, y: nat
binary x ∸ binary y = binary (x ∸ y)
  Proof.
x, y: nat
binary x ∸ binary y = binary (x ∸ y)
    revert y; induction x; intros y; induction y; try reflexivity.
y: nat
IHy: binary 0 ∸ binary y = binary (0%nat ∸ y)
binary 0 ∸ binary y.+1 = binary (0%nat ∸ y.+1%nat)
x: nat
IHx: forall y : nat, binary x ∸ binary y = binary (x ∸ y)
binary x.+1 ∸ binary 0 = binary (x.+1%nat ∸ 0%nat)
x: nat
IHx: forall y : nat, binary x ∸ binary y = binary (x ∸ y)
y: nat
IHy: binary x.+1 ∸ binary y = binary (x.+1%nat ∸ y)
binary x.+1 ∸ binary y.+1 =
binary (x.+1%nat ∸ y.+1%nat)
    -
y: nat
IHy: binary 0 ∸ binary y = binary (0%nat ∸ y)
binary 0 ∸ binary y.+1 = binary (0%nat ∸ y.+1%nat) apply binnat_zero_minus.
    -
x: nat
IHx: forall y : nat, binary x ∸ binary y = binary (x ∸ y)
binary x.+1 ∸ binary 0 = binary (x.+1%nat ∸ 0%nat) apply binnat_minus_zero.
    -
x: nat
IHx: forall y : nat, binary x ∸ binary y = binary (x ∸ y)
y: nat
IHy: binary x.+1 ∸ binary y = binary (x.+1%nat ∸ y)
binary x.+1 ∸ binary y.+1 =
binary (x.+1%nat ∸ y.+1%nat) simpl in *.
x: nat
IHx: forall y : nat, binary x ∸ binary y = binary (x ∸ y)
y: nat
IHy: Succ (binary x) ∸ binary y = binary (x.+1%nat ∸ y)
Succ (binary x) ∸ Succ (binary y) =
binary (x.+1%nat ∸ y.+1%nat) rewrite binnat_minus_succ.
x: nat
IHx: forall y : nat, binary x ∸ binary y = binary (x ∸ y)
y: nat
IHy: Succ (binary x) ∸ binary y = binary (x.+1%nat ∸ y)
binary x ∸ binary y = binary (x.+1%nat ∸ y.+1%nat)
      rewrite IHx.
x: nat
IHx: forall y : nat, binary x ∸ binary y = binary (x ∸ y)
y: nat
IHy: Succ (binary x) ∸ binary y = binary (x.+1%nat ∸ y)
binary (x ∸ y) = binary (x.+1%nat ∸ y.+1%nat) reflexivity.
  Qed.

  Local Definition unaryminus (m n : binnat) : unary m ∸ unary n = unary (m ∸ n).
m, n: binnat
binary^-1 m ∸ binary^-1 n = binary^-1 (m ∸ n)
  Proof.
m, n: binnat
binary^-1 m ∸ binary^-1 n = binary^-1 (m ∸ n)
    etransitivity (unary (binary (_^-1 m ∸ _^-1 n))).
m, n: binnat
binary^-1 m ∸ binary^-1 n =
equiv_binary^-1 (binary (?f^-1 m ∸ ?f0^-1 n))
m, n: binnat
equiv_binary^-1 (binary (?f^-1 m ∸ ?f0^-1 n)) =
binary^-1 (m ∸ n)
    -
m, n: binnat
binary^-1 m ∸ binary^-1 n =
equiv_binary^-1 (binary (?f^-1 m ∸ ?f0^-1 n)) apply ((eissect binary (unary m ∸ unary n)) ^).
    -
m, n: binnat
binary^-1 (binary (binary^-1 m ∸ binary^-1 n)) =
binary^-1 (m ∸ n) rewrite <- binaryminus.
m, n: binnat
binary^-1
  (binary (binary^-1 m) ∸ binary (binary^-1 n)) =
binary^-1 (m ∸ n)
      rewrite (eisretr binary m), (eisretr binary n).
m, n: binnat
binary^-1 (m ∸ n) = binary^-1 (m ∸ n)
      reflexivity.
  Qed.

  #[export] Instance binnat_cut_minus_spec : CutMinusSpec binnat binnat_cut_minus.
CutMinusSpec binnat binnat_cut_minus
  Proof.
CutMinusSpec binnat binnat_cut_minus
    split.
forall x y : binnat, y ≤ x -> x ∸ y + y = x
forall x y : binnat, x ≤ y -> x ∸ y = 0
    -
forall x y : binnat, y ≤ x -> x ∸ y + y = x intros m n E.
m, n: binnat
E: n ≤ m
m ∸ n + n = m apply (equiv_inj unary).
m, n: binnat
E: n ≤ m
binary^-1 (m ∸ n + n) = binary^-1 m
      rewrite <- unaryplus, <- unaryminus.
m, n: binnat
E: n ≤ m
binary^-1 m ∸ binary^-1 n + binary^-1 n = binary^-1 m
      apply nat_cut_minus_spec.
m, n: binnat
E: n ≤ m
binary^-1 n ≤ binary^-1 m
      assumption.
    -
forall x y : binnat, x ≤ y -> x ∸ y = 0 intros m n E.
m, n: binnat
E: m ≤ n
m ∸ n = 0 apply (equiv_inj unary).
m, n: binnat
E: m ≤ n
binary^-1 (m ∸ n) = binary^-1 0
      rewrite <- unaryminus.
m, n: binnat
E: m ≤ n
binary^-1 m ∸ binary^-1 n = binary^-1 0
      apply nat_cut_minus_spec.
m, n: binnat
E: m ≤ n
binary^-1 m ≤ binary^-1 n
      assumption.
  Qed.

End minus.