diff --git a/Everything/Safe.agda b/Everything/Safe.agda
index 9f952f1..41d1b88 100644
--- a/Everything/Safe.agda
+++ b/Everything/Safe.agda
@@ -6,6 +6,7 @@ open import Numbers.Naturals.Naturals
 open import Numbers.BinaryNaturals.Definition
 open import Numbers.BinaryNaturals.Multiplication
 open import Numbers.BinaryNaturals.Order
+open import Numbers.BinaryNaturals.Subtraction
 
 open import Numbers.Integers.Integers
 
diff --git a/Maybe.agda b/Maybe.agda
index 0452905..5daa33d 100644
--- a/Maybe.agda
+++ b/Maybe.agda
@@ -35,5 +35,5 @@ module Maybe where
   noNotYes : {a : _} {A : Set a} {b : A} → (no ≡ yes b) → False
   noNotYes ()
 
-  mapMaybePreservesNo : {a b : _} {A : Set a} {B : Set b} (f : A → B) (x : Maybe A) → mapMaybe f x ≡ no → x ≡ no
-  mapMaybePreservesNo f no pr = refl
+  mapMaybePreservesNo : {a b : _} {A : Set a} {B : Set b} {f : A → B} {x : Maybe A} → mapMaybe f x ≡ no → x ≡ no
+  mapMaybePreservesNo {f = f} {no} pr = refl
diff --git a/Numbers/BinaryNaturals/Definition.agda b/Numbers/BinaryNaturals/Definition.agda
index 624da8e..fa50f69 100644
--- a/Numbers/BinaryNaturals/Definition.agda
+++ b/Numbers/BinaryNaturals/Definition.agda
@@ -86,6 +86,12 @@ module Numbers.BinaryNaturals.Definition where
   binNatToNZero : (x : BinNat) → binNatToN x ≡ 0 → canonical x ≡ []
   binNatToNZero' : (x : BinNat) → canonical x ≡ [] → binNatToN x ≡ 0
 
+  NToBinNatZero : (n : ℕ) → NToBinNat n ≡ [] → n ≡ 0
+  NToBinNatZero zero pr = refl
+  NToBinNatZero (succ n) pr with NToBinNat n
+  NToBinNatZero (succ n) pr | zero :: bl = exFalso (nonEmptyNotEmpty pr)
+  NToBinNatZero (succ n) pr | one :: bl = exFalso (nonEmptyNotEmpty pr)
+
   canonicalAscends : {i : Bit} → (a : BinNat) → 0 <N binNatToN a → i :: canonical a ≡ canonical (i :: a)
 
   canonicalAscends' : {i : Bit} → (a : BinNat) → (canonical a ≡ [] → False) → i :: canonical a ≡ canonical (i :: a)
diff --git a/Numbers/BinaryNaturals/Order.agda b/Numbers/BinaryNaturals/Order.agda
index 29873db..afb46fd 100644
--- a/Numbers/BinaryNaturals/Order.agda
+++ b/Numbers/BinaryNaturals/Order.agda
@@ -1,5 +1,6 @@
 {-# OPTIONS --warning=error --safe --without-K #-}
 
+open import WellFoundedInduction
 open import LogicalFormulae
 open import Functions
 open import Lists.Lists
@@ -16,6 +17,15 @@ module Numbers.BinaryNaturals.Order where
     FirstLess : Compare
     FirstGreater : Compare
 
+  badCompare : Equal ≡ FirstLess → False
+  badCompare ()
+
+  badCompare' : Equal ≡ FirstGreater → False
+  badCompare' ()
+
+  badCompare'' : FirstLess ≡ FirstGreater → False
+  badCompare'' ()
+
   _<BInherited_ : BinNat → BinNat → Compare
   a <BInherited b with orderIsTotal (binNatToN a) (binNatToN b)
   (a <BInherited b) | inl (inl x) = FirstLess
@@ -195,6 +205,25 @@ module Numbers.BinaryNaturals.Order where
   equalContaminated' (one :: n) (zero :: m) pr = equalContaminated' n m pr
   equalContaminated' (one :: n) (one :: m) pr = equalContaminated' n m pr
 
+  comparisonEqual : (a b : BinNat) → (a <B b ≡ Equal) → canonical a ≡ canonical b
+  comparisonEqual [] [] pr = refl
+  comparisonEqual [] (zero :: b) pr with inspect (canonical b)
+  comparisonEqual [] (zero :: b) pr | [] with≡ p rewrite p = refl
+  comparisonEqual [] (zero :: b) pr | (x :: r) with≡ p rewrite zeroLess b (λ i → nonEmptyNotEmpty (transitivity (equalityCommutative p) i)) = exFalso (badCompare (equalityCommutative pr))
+  comparisonEqual (zero :: a) [] pr with inspect (canonical a)
+  comparisonEqual (zero :: a) [] pr | [] with≡ x rewrite x = refl
+  comparisonEqual (zero :: a) [] pr | (x₁ :: y) with≡ x rewrite zeroLess' a (λ i → nonEmptyNotEmpty (transitivity (equalityCommutative x) i)) = exFalso (badCompare' (equalityCommutative pr))
+  comparisonEqual (zero :: a) (zero :: b) pr with inspect (canonical a)
+  comparisonEqual (zero :: a) (zero :: b) pr | [] with≡ x with inspect (canonical b)
+  comparisonEqual (zero :: a) (zero :: b) pr | [] with≡ pr2 | [] with≡ pr3 rewrite pr2 | pr3 = refl
+  comparisonEqual (zero :: a) (zero :: b) pr | [] with≡ pr2 | (x₂ :: y) with≡ pr3 rewrite pr2 | pr3 | comparisonEqual a b pr = exFalso (nonEmptyNotEmpty (transitivity (equalityCommutative pr3) pr2))
+  comparisonEqual (zero :: a) (zero :: b) pr | (c :: cs) with≡ pr2 with inspect (canonical b)
+  comparisonEqual (zero :: a) (zero :: b) pr | (c :: cs) with≡ pr2 | [] with≡ pr3 rewrite pr2 | pr3 | comparisonEqual a b pr = exFalso (nonEmptyNotEmpty (transitivity (equalityCommutative pr2) pr3))
+  comparisonEqual (zero :: a) (zero :: b) pr | (c :: cs) with≡ pr2 | (x₁ :: y) with≡ pr3 rewrite pr2 | pr3 | comparisonEqual a b pr = applyEquality (zero ::_) (transitivity (equalityCommutative pr2) pr3)
+  comparisonEqual (zero :: a) (one :: b) pr = exFalso (equalContaminated a b pr)
+  comparisonEqual (one :: a) (zero :: b) pr = exFalso (equalContaminated' a b pr)
+  comparisonEqual (one :: a) (one :: b) pr = applyEquality (one ::_) (comparisonEqual a b pr)
+
   equalSymmetric : (n m : BinNat) → n <B m ≡ Equal → m <B n ≡ Equal
   equalSymmetric [] [] n=m = refl
   equalSymmetric [] (zero :: m) n=m rewrite equalSymmetric [] m n=m = refl
diff --git a/Numbers/BinaryNaturals/Subtraction.agda b/Numbers/BinaryNaturals/Subtraction.agda
new file mode 100644
index 0000000..3fc155a
--- /dev/null
+++ b/Numbers/BinaryNaturals/Subtraction.agda
@@ -0,0 +1,464 @@
+{-# OPTIONS --warning=error --safe --without-K #-}
+
+open import LogicalFormulae
+open import Lists.Lists
+open import Numbers.Naturals.Naturals
+open import Numbers.Naturals.Order
+open import Numbers.BinaryNaturals.Definition
+open import Numbers.BinaryNaturals.Addition
+open import Numbers.BinaryNaturals.SubtractionGo
+open import Numbers.BinaryNaturals.SubtractionGoPreservesCanonicalRight
+open import Numbers.BinaryNaturals.SubtractionGoPreservesCanonicalLeft
+open import Orders
+open import Semirings.Definition
+open import Maybe
+
+module Numbers.BinaryNaturals.Subtraction where
+
+  aMinusAGo : (a : BinNat) → mapMaybe canonical (go zero a a) ≡ yes []
+  aMinusAGo [] = refl
+  aMinusAGo (zero :: a) with aMinusAGo a
+  ... | bl with go zero a a
+  aMinusAGo (zero :: a) | bl | yes x rewrite yesInjective bl = refl
+  aMinusAGo (one :: a) with aMinusAGo a
+  ... | bl with go zero a a
+  aMinusAGo (one :: a) | bl | yes x rewrite yesInjective bl = refl
+
+  aMinusALemma : (a : BinNat) → mapMaybe canonical (mapMaybe (_::_ zero) (go zero a a)) ≡ yes []
+  aMinusALemma a with inspect (go zero a a)
+  aMinusALemma a | no with≡ x with aMinusAGo a
+  ... | r rewrite x = exFalso (noNotYes r)
+  aMinusALemma a | yes xs with≡ pr with inspect (canonical xs)
+  aMinusALemma a | yes xs with≡ pr | [] with≡ pr2 rewrite pr | pr2 = refl
+  aMinusALemma a | yes xs with≡ pr | (x :: t) with≡ pr2 with aMinusAGo a
+  ... | b rewrite pr | pr2 = exFalso (nonEmptyNotEmpty (yesInjective b))
+
+  aMinusA : (a : BinNat) → mapMaybe canonical (a -B a) ≡ yes []
+  aMinusA [] = refl
+  aMinusA (zero :: a) = aMinusALemma a
+  aMinusA (one :: a) = aMinusALemma a
+
+  goOne : (a b : BinNat) → mapMaybe canonical (go one (incr a) b) ≡ mapMaybe canonical (go zero a b)
+  goOne [] [] = refl
+  goOne [] (zero :: b) with inspect (go zero [] b)
+  goOne [] (zero :: b) | no with≡ pr rewrite pr = refl
+  goOne [] (zero :: b) | yes x with≡ pr with goZeroEmpty b pr
+  ... | t with inspect (canonical x)
+  goOne [] (zero :: b) | yes x with≡ pr | t | [] with≡ pr2 rewrite pr | pr2 = refl
+  goOne [] (zero :: b) | yes x with≡ pr | t | (x₁ :: y) with≡ pr2 with goZeroEmpty' b pr
+  ... | bl = exFalso (nonEmptyNotEmpty (transitivity (equalityCommutative pr2) bl))
+  goOne [] (one :: b) with inspect (go one [] b)
+  goOne [] (one :: b) | no with≡ pr rewrite pr = refl
+  goOne [] (one :: b) | yes x with≡ pr = exFalso (goOneEmpty b pr)
+  goOne (zero :: a) [] = refl
+  goOne (zero :: a) (zero :: b) = refl
+  goOne (zero :: a) (one :: b) = refl
+  goOne (one :: a) [] with inspect (go one (incr a) [])
+  goOne (one :: a) [] | no with≡ pr with goOne a []
+  ... | bl rewrite pr | goEmpty a = exFalso (noNotYes bl)
+  goOne (one :: a) [] | yes y with≡ pr with goOne a []
+  ... | bl rewrite pr = applyEquality (λ i → yes (one :: i)) (yesInjective (transitivity bl (applyEquality (mapMaybe canonical) (goEmpty a))))
+  goOne (one :: a) (zero :: b) with inspect (go zero a b)
+  goOne (one :: a) (zero :: b) | no with≡ pr with inspect (go one (incr a) b)
+  goOne (one :: a) (zero :: b) | no with≡ pr | no with≡ x rewrite pr | x = refl
+  goOne (one :: a) (zero :: b) | no with≡ pr | yes y with≡ x with goOne a b
+  ... | f rewrite pr | x = exFalso (noNotYes (equalityCommutative f))
+  goOne (one :: a) (zero :: b) | yes y with≡ pr with inspect (go one (incr a) b)
+  goOne (one :: a) (zero :: b) | yes y with≡ pr | no with≡ x with goOne a b
+  ... | f rewrite pr | x = exFalso (noNotYes f)
+  goOne (one :: a) (zero :: b) | yes y with≡ pr | yes z with≡ x rewrite pr | x = applyEquality (λ i → yes (one :: i)) (yesInjective (transitivity (transitivity (applyEquality (mapMaybe canonical) (equalityCommutative x)) (goOne a b)) (applyEquality (mapMaybe canonical) pr)))
+  goOne (one :: a) (one :: b) with inspect (go zero a b)
+  goOne (one :: a) (one :: b) | no with≡ pr with inspect (go one (incr a) b)
+  goOne (one :: a) (one :: b) | no with≡ pr | no with≡ pr2 rewrite pr | pr2 = refl
+  goOne (one :: a) (one :: b) | no with≡ pr | yes x with≡ pr2 rewrite pr | pr2 = exFalso (noNotYes (transitivity (applyEquality (mapMaybe canonical) (equalityCommutative pr)) (transitivity (equalityCommutative (goOne a b)) (applyEquality (mapMaybe canonical) pr2))))
+  goOne (one :: a) (one :: b) | yes y with≡ pr with inspect (go one (incr a) b)
+  goOne (one :: a) (one :: b) | yes y with≡ pr | yes z with≡ pr2 rewrite pr | pr2 = applyEquality yes t
+    where
+      u : canonical z ≡ canonical y
+      u = yesInjective (transitivity (transitivity (equalityCommutative (applyEquality (mapMaybe canonical) pr2)) (goOne a b)) (applyEquality (mapMaybe canonical) pr))
+      t : canonical (zero :: z) ≡ canonical (zero :: y)
+      t with inspect (canonical z)
+      t | [] with≡ pr1 rewrite equalityCommutative u | pr1 = refl
+      t | (x :: bl) with≡ pr rewrite equalityCommutative u | pr = refl
+  goOne (one :: a) (one :: b) | yes y with≡ pr | no with≡ pr2 rewrite pr | pr2 = exFalso (noNotYes (transitivity (equalityCommutative (applyEquality (mapMaybe canonical) pr2)) (transitivity (goOne a b) (applyEquality (mapMaybe canonical) pr))))
+
+  plusThenMinus : (a b : BinNat) → mapMaybe canonical ((a +B b) -B b) ≡ yes (canonical a)
+  plusThenMinus [] b = aMinusA b
+  plusThenMinus (zero :: a) [] = refl
+  plusThenMinus (zero :: a) (zero :: b) = t
+    where
+      t : mapMaybe canonical (mapMaybe (zero ::_) (go zero (a +B b) b)) ≡ yes (canonical (zero :: a))
+      t with inspect (go zero (a +B b) b)
+      t | no with≡ x with plusThenMinus a b
+      ... | bl rewrite x = exFalso (noNotYes bl)
+      t | yes y with≡ x with plusThenMinus a b
+      ... | f rewrite x = applyEquality yes u
+        where
+          u : canonical (zero :: y) ≡ canonical (zero :: a)
+          u with inspect (canonical y)
+          u | [] with≡ pr rewrite pr | equalityCommutative (yesInjective f) = refl
+          u | (x :: bl) with≡ pr rewrite pr | equalityCommutative (yesInjective f) = refl
+  plusThenMinus (zero :: a) (one :: b) = t
+    where
+      t : mapMaybe canonical (mapMaybe (zero ::_) (go zero (a +B b) b)) ≡ yes (canonical (zero :: a))
+      t with inspect (go zero (a +B b) b)
+      t | no with≡ x with plusThenMinus a b
+      ... | bl rewrite x = exFalso (noNotYes bl)
+      t | yes y with≡ x with plusThenMinus a b
+      ... | f rewrite x = applyEquality yes u
+        where
+          u : canonical (zero :: y) ≡ canonical (zero :: a)
+          u with inspect (canonical y)
+          u | [] with≡ pr rewrite pr | equalityCommutative (yesInjective f) = refl
+          u | (x :: bl) with≡ pr rewrite pr | equalityCommutative (yesInjective f) = refl
+  plusThenMinus (one :: a) [] = refl
+  plusThenMinus (one :: a) (zero :: b) = t
+    where
+      t : mapMaybe canonical (mapMaybe (_::_ one) (go zero (a +B b) b)) ≡ yes (one :: canonical a)
+      t with inspect (go zero (a +B b) b)
+      t | no with≡ x with plusThenMinus a b
+      ... | bl rewrite x = exFalso (noNotYes bl)
+      t | yes y with≡ x with plusThenMinus a b
+      ... | bl rewrite x = applyEquality (λ i → yes (one :: i)) (yesInjective bl)
+  plusThenMinus (one :: a) (one :: b) = t
+    where
+      t : mapMaybe canonical (mapMaybe (_::_ one) (go one (incr (a +B b)) b)) ≡ yes (one :: canonical a)
+      t with inspect (go one (incr (a +B b)) b)
+      t | no with≡ x with goOne (a +B b) b
+      ... | f rewrite x | plusThenMinus a b = exFalso (noNotYes f)
+      t | yes y with≡ x with goOne (a +B b) b
+      ... | f rewrite x | plusThenMinus a b = applyEquality (λ i → yes (one :: i)) (yesInjective f)
+
+  subLemma : (a b : ℕ) → a <N b → succ (a +N a) <N b +N b
+  subLemma a b a<b with TotalOrder.totality ℕTotalOrder (succ (a +N a)) (b +N b)
+  subLemma a b a<b | inl (inl x) = x
+  subLemma a b a<b | inl (inr x) = exFalso (noIntegersBetweenXAndSuccX (a +N a) (addStrongInequalities a<b a<b) x)
+  subLemma a b a<b | inr x = exFalso (parity a b (transitivity (applyEquality (succ a +N_) (Semiring.sumZeroRight ℕSemiring a)) (transitivity x (applyEquality (b +N_) (equalityCommutative (Semiring.sumZeroRight ℕSemiring b))))))
+
+  subLemma2 : (a b : ℕ) → a <N b → 2 *N a <N succ (2 *N b)
+  subLemma2 a b a<b with TotalOrder.totality ℕTotalOrder (2 *N a) (succ (2 *N b))
+  subLemma2 a b a<b | inl (inl x) = x
+  subLemma2 a b a<b | inl (inr x) = exFalso (TotalOrder.irreflexive ℕTotalOrder (TotalOrder.transitive ℕTotalOrder x (TotalOrder.transitive ℕTotalOrder (lessRespectsMultiplicationLeft a b 2 a<b (le 1 refl)) (le 0 refl))))
+  subLemma2 a b a<b | inr x = exFalso (parity b a (equalityCommutative x))
+
+  subtraction : (a b : BinNat) → a -B b ≡ no → binNatToN a <N binNatToN b
+  subtraction' : (a b : BinNat) → go one a b ≡ no → (binNatToN a <N binNatToN b) || (binNatToN a ≡ binNatToN b)
+
+  subtraction' [] [] pr = inr refl
+  subtraction' [] (x :: b) pr with TotalOrder.totality ℕTotalOrder 0 (binNatToN (x :: b))
+  subtraction' [] (x :: b) pr | inl (inl x₁) = inl x₁
+  subtraction' [] (x :: b) pr | inr x₁ = inr x₁
+  subtraction' (zero :: a) [] pr with subtraction' a [] (mapMaybePreservesNo pr)
+  subtraction' (zero :: a) [] pr | inr x rewrite x = inr refl
+  subtraction' (zero :: a) (zero :: b) pr with subtraction' a b (mapMaybePreservesNo pr)
+  subtraction' (zero :: a) (zero :: b) pr | inl x = inl (lessRespectsMultiplicationLeft (binNatToN a) (binNatToN b) 2 x (le 1 refl))
+  subtraction' (zero :: a) (zero :: b) pr | inr x rewrite x = inr refl
+  subtraction' (zero :: a) (one :: b) pr with subtraction' a b (mapMaybePreservesNo pr)
+  subtraction' (zero :: a) (one :: b) pr | inl x = inl (subLemma2 (binNatToN a) (binNatToN b) x)
+  subtraction' (zero :: a) (one :: b) pr | inr x rewrite x = inl (le zero refl)
+  subtraction' (one :: a) (zero :: b) pr with subtraction a b (mapMaybePreservesNo pr)
+  ... | t rewrite Semiring.sumZeroRight ℕSemiring (binNatToN a) | Semiring.sumZeroRight ℕSemiring (binNatToN b) = inl (subLemma (binNatToN a) (binNatToN b) t)
+  subtraction' (one :: a) (one :: b) pr with subtraction' a b (mapMaybePreservesNo pr)
+  subtraction' (one :: a) (one :: b) pr | inl x = inl (succPreservesInequality (lessRespectsMultiplicationLeft (binNatToN a) (binNatToN b) 2 x (le 1 refl)))
+  subtraction' (one :: a) (one :: b) pr | inr x rewrite x = inr refl
+
+  subtraction [] (zero :: b) pr with inspect (binNatToN b)
+  subtraction [] (zero :: b) pr | zero with≡ pr1 = exFalso (noNotYes (transitivity (applyEquality (mapMaybe canonical) (equalityCommutative pr)) (transitivity (goPreservesCanonicalRight zero [] b) (transitivity (applyEquality (λ i → mapMaybe canonical (go zero [] i)) (binNatToNZero b pr1)) refl))))
+  subtraction [] (zero :: b) pr | (succ bl) with≡ pr1 rewrite pr | pr1 = succIsPositive _
+  subtraction [] (one :: b) pr = succIsPositive _
+  subtraction (zero :: a) (zero :: b) pr = lessRespectsMultiplicationLeft (binNatToN a) (binNatToN b) 2 u (le 1 refl)
+    where
+      u : binNatToN a <N binNatToN b
+      u = subtraction a b (mapMaybePreservesNo pr)
+  subtraction (zero :: a) (one :: b) pr with subtraction' a b (mapMaybePreservesNo pr)
+  subtraction (zero :: a) (one :: b) pr | inl x = subLemma2 (binNatToN a) (binNatToN b) x
+  subtraction (zero :: a) (one :: b) pr | inr x rewrite x = le zero refl
+  subtraction (one :: a) (zero :: b) pr rewrite Semiring.sumZeroRight ℕSemiring (binNatToN a) | Semiring.sumZeroRight ℕSemiring (binNatToN b) = subLemma (binNatToN a) (binNatToN b) u
+    where
+      u : binNatToN a <N binNatToN b
+      u = subtraction a b (mapMaybePreservesNo pr)
+  subtraction (one :: a) (one :: b) pr = succPreservesInequality (lessRespectsMultiplicationLeft (binNatToN a) (binNatToN b) 2 u (le 1 refl))
+    where
+      u : binNatToN a <N binNatToN b
+      u = subtraction a b (mapMaybePreservesNo pr)
+
+  subLemma4 : (a b : BinNat) {t : BinNat} → go one a b ≡ no → go zero a b ≡ yes t → canonical t ≡ []
+  subLemma4 [] [] {t} pr1 pr2 rewrite yesInjective (equalityCommutative pr2) = refl
+  subLemma4 [] (x :: b) {t} pr1 pr2 = goZeroEmpty' (x :: b) pr2
+  subLemma4 (zero :: a) [] {t} pr1 pr2 with inspect (go one a [])
+  subLemma4 (zero :: a) [] {t} pr1 pr2 | no with≡ pr3 with subLemma4 a [] pr3 (goEmpty a)
+  ... | bl with applyEquality canonical (yesInjective pr2)
+  ... | th rewrite bl = equalityCommutative th
+  subLemma4 (zero :: a) [] {t} pr1 pr2 | yes x with≡ pr3 rewrite pr3 = exFalso (noNotYes (equalityCommutative pr1))
+  subLemma4 (zero :: a) (zero :: b) {t} pr1 pr2 with inspect (go one a b)
+  subLemma4 (zero :: a) (zero :: b) {t} pr1 pr2 | no with≡ pr3 with inspect (go zero a b)
+  subLemma4 (zero :: a) (zero :: b) {t} pr1 pr2 | no with≡ pr3 | no with≡ pr4 rewrite pr4 = exFalso (noNotYes pr2)
+  subLemma4 (zero :: a) (zero :: b) {t} pr1 pr2 | no with≡ pr3 | yes x with≡ pr4 with subLemma4 a b pr3 pr4
+  ... | bl rewrite pr3 | pr4 = ans
+    where
+      ans : canonical t ≡ []
+      ans rewrite equalityCommutative (applyEquality canonical (yesInjective pr2)) | bl = refl
+  subLemma4 (zero :: a) (zero :: b) {t} pr1 pr2 | yes x with≡ pr3 rewrite pr3 = exFalso (noNotYes (equalityCommutative pr1))
+  subLemma4 (zero :: a) (one :: b) {t} pr1 pr2 with go one a b
+  ... | no = exFalso (noNotYes pr2)
+  subLemma4 (zero :: a) (one :: b) {t} pr1 pr2 | yes x = exFalso (noNotYes (equalityCommutative pr1))
+  subLemma4 (one :: a) (zero :: b) {t} pr1 pr2 with go zero a b
+  subLemma4 (one :: a) (zero :: b) {t} pr1 pr2 | no = exFalso (noNotYes pr2)
+  subLemma4 (one :: a) (zero :: b) {t} pr1 pr2 | yes x = exFalso (noNotYes (equalityCommutative pr1))
+  subLemma4 (one :: a) (one :: b) {t} pr1 pr2 with inspect (go zero a b)
+  subLemma4 (one :: a) (one :: b) {t} pr1 pr2 | no with≡ pr3 rewrite pr3 = exFalso (noNotYes pr2)
+  subLemma4 (one :: a) (one :: b) {t} pr1 pr2 | yes x with≡ pr3 with inspect (go one a b)
+  subLemma4 (one :: a) (one :: b) {t} pr1 pr2 | yes x with≡ pr3 | no with≡ pr4 with subLemma4 a b pr4 pr3
+  ... | bl rewrite pr3 | pr4 | bl = ans
+    where
+      ans : canonical t ≡ []
+      ans rewrite equalityCommutative (applyEquality canonical (yesInjective pr2)) | bl = refl
+  subLemma4 (one :: a) (one :: b) {t} pr1 pr2 | yes x with≡ pr3 | yes x₁ with≡ pr4 rewrite pr4 = exFalso (noNotYes (equalityCommutative pr1))
+
+  goOneFromZero : (a b : BinNat) → go zero a b ≡ no → go one a b ≡ no
+  goOneFromZero [] (zero :: b) pr = refl
+  goOneFromZero [] (one :: b) pr = refl
+  goOneFromZero (zero :: a) (zero :: b) pr rewrite goOneFromZero a b (mapMaybePreservesNo pr) = refl
+  goOneFromZero (zero :: a) (one :: b) pr rewrite (mapMaybePreservesNo pr) = refl
+  goOneFromZero (one :: a) (zero :: b) pr rewrite (mapMaybePreservesNo pr) = refl
+  goOneFromZero (one :: a) (one :: b) pr rewrite goOneFromZero a b (mapMaybePreservesNo pr) = refl
+
+  subLemma5 : (a b : BinNat) → mapMaybe canonical (go zero a b) ≡ yes [] → go one a b ≡ no
+  subLemma5 [] b pr = goOneEmpty' b
+  subLemma5 (zero :: a) [] pr with inspect (canonical a)
+  subLemma5 (zero :: a) [] pr | (z :: zs) with≡ pr2 rewrite pr2 = exFalso (nonEmptyNotEmpty (yesInjective pr))
+  subLemma5 (zero :: a) [] pr | [] with≡ pr2 rewrite pr2 = applyEquality (mapMaybe (one ::_)) (subLemma5 a [] (transitivity (applyEquality (mapMaybe canonical) (goEmpty a)) (applyEquality yes pr2)))
+  subLemma5 (zero :: a) (zero :: b) pr with inspect (go zero a b)
+  subLemma5 (zero :: a) (zero :: b) pr | no with≡ pr2 rewrite pr2 = exFalso (noNotYes pr)
+  subLemma5 (zero :: a) (zero :: b) pr | yes x with≡ pr2 with inspect (canonical x)
+  subLemma5 (zero :: a) (zero :: b) pr | yes x with≡ pr2 | [] with≡ pr3 rewrite pr | pr2 | pr3 = applyEquality (mapMaybe (one ::_)) (subLemma5 a b (transitivity (applyEquality (mapMaybe canonical) pr2) (applyEquality yes pr3)))
+  subLemma5 (zero :: a) (zero :: b) pr | yes x with≡ pr2 | (x₁ :: bl) with≡ pr3 rewrite pr | pr2 | pr3 = exFalso (nonEmptyNotEmpty (yesInjective pr))
+  subLemma5 (zero :: a) (one :: b) pr with (go one a b)
+  subLemma5 (zero :: a) (one :: b) pr | no = exFalso (noNotYes pr)
+  subLemma5 (zero :: a) (one :: b) pr | yes y = exFalso (nonEmptyNotEmpty (yesInjective pr))
+  subLemma5 (one :: a) (zero :: b) pr with go zero a b
+  subLemma5 (one :: a) (zero :: b) pr | no = exFalso (noNotYes pr)
+  subLemma5 (one :: a) (zero :: b) pr | yes x = exFalso (nonEmptyNotEmpty (yesInjective pr))
+  subLemma5 (one :: a) (one :: b) pr with inspect (go zero a b)
+  subLemma5 (one :: a) (one :: b) pr | yes x with≡ pr2 with inspect (canonical x)
+  subLemma5 (one :: a) (one :: b) pr | yes x with≡ pr2 | [] with≡ pr3 rewrite pr | pr2 | pr3 = applyEquality (mapMaybe (one ::_)) (subLemma5 a b (transitivity (applyEquality (mapMaybe canonical) pr2) (applyEquality yes pr3)))
+  subLemma5 (one :: a) (one :: b) pr | yes x with≡ pr2 | (x₁ :: y) with≡ pr3 rewrite pr | pr2 | pr3 = exFalso (nonEmptyNotEmpty (yesInjective pr))
+  subLemma5 (one :: a) (one :: b) pr | no with≡ pr2 rewrite pr2 = exFalso (noNotYes pr)
+
+  subLemma3 : (a b : BinNat) → go zero a b ≡ no → (go zero (incr a) b ≡ no) || (mapMaybe canonical (go zero (incr a) b) ≡ yes [])
+  subLemma3 a b pr with inspect (go zero (incr a) b)
+  subLemma3 a b pr | no with≡ x = inl x
+  subLemma3 [] (zero :: b) pr | yes y with≡ pr1 rewrite pr = exFalso (noNotYes pr1)
+  subLemma3 [] (one :: b) pr | yes y with≡ pr1 with inspect (go zero [] b)
+  subLemma3 [] (one :: b) pr | yes y with≡ pr1 | no with≡ pr2 rewrite pr1 | pr2 = exFalso (noNotYes pr1)
+  subLemma3 [] (one :: b) pr | yes y with≡ pr1 | yes x with≡ pr2 with goZeroEmpty' b pr2
+  ... | f rewrite pr1 | pr2 | equalityCommutative (yesInjective pr1) | f = inr refl
+  subLemma3 (zero :: a) (zero :: b) pr | yes y with≡ pr1 rewrite mapMaybePreservesNo pr = exFalso (noNotYes pr1)
+  subLemma3 (zero :: a) (one :: b) pr | yes y with≡ pr1 with inspect (go zero a b)
+  subLemma3 (zero :: a) (one :: b) pr | yes y with≡ pr1 | no with≡ pr2 rewrite pr1 | pr2 = exFalso (noNotYes pr1)
+  subLemma3 (zero :: a) (one :: b) pr | yes y with≡ pr1 | yes x with≡ pr2 with inspect (canonical x)
+  ... | [] with≡ pr3 rewrite pr1 | pr2 | equalityCommutative (yesInjective pr1) | pr3 = inr refl
+  ... | (z :: zs) with≡ pr3 with inspect (go one a b)
+  subLemma3 (zero :: a) (one :: b) pr | yes y with≡ pr1 | yes x with≡ pr2 | (z :: zs) with≡ pr3 | no with≡ pr4 rewrite pr1 | pr2 | pr3 | pr4 = exFalso (nonEmptyNotEmpty (transitivity (equalityCommutative pr3) (subLemma4 a b pr4 pr2)))
+  subLemma3 (zero :: a) (one :: b) pr | yes y with≡ pr1 | yes x with≡ pr2 | (z :: zs) with≡ pr3 | yes x₁ with≡ pr4 rewrite pr1 | pr2 | pr3 | pr4 = exFalso (noNotYes (equalityCommutative pr))
+  subLemma3 (one :: a) (zero :: b) pr | yes y with≡ pr1 with subLemma3 a b (mapMaybePreservesNo pr)
+  subLemma3 (one :: a) (zero :: b) pr | yes y with≡ pr1 | inl x rewrite x = inl refl
+  subLemma3 (one :: a) (zero :: b) pr | yes y with≡ pr1 | inr x with inspect (go zero (incr a) b)
+  ... | no with≡ pr2 rewrite pr1 | pr2 = exFalso (noNotYes x)
+  ... | yes z with≡ pr2 rewrite pr1 | pr2 = inr (applyEquality yes (transitivity (transitivity (applyEquality canonical (yesInjective (equalityCommutative pr1))) r) (yesInjective x)))
+    where
+      r : canonical (zero :: z) ≡ canonical z
+      r rewrite yesInjective x = refl
+  subLemma3 (one :: a) (one :: b) pr | yes y with≡ pr1 with subLemma3 a b (mapMaybePreservesNo pr)
+  subLemma3 (one :: a) (one :: b) pr | yes y with≡ pr1 | inl x with inspect (go one (incr a) b)
+  subLemma3 (one :: a) (one :: b) pr | yes y with≡ pr1 | inl th | no with≡ pr2 rewrite pr2 = exFalso (noNotYes pr1)
+  subLemma3 (one :: a) (one :: b) pr | yes y with≡ pr1 | inl th | yes x with≡ pr2 with goOneFromZero (incr a) b th
+  ... | bad rewrite pr2 = exFalso (noNotYes (equalityCommutative bad))
+  subLemma3 (one :: a) (one :: b) pr | yes y with≡ pr1 | inr x with inspect (go one (incr a) b)
+  subLemma3 (one :: a) (one :: b) pr | yes y with≡ pr1 | inr x | no with≡ pr2 rewrite pr2 = exFalso (noNotYes pr1)
+  subLemma3 (one :: a) (one :: b) pr | yes y with≡ pr1 | inr th | yes z with≡ pr2 with inspect (go zero (incr a) b)
+  subLemma3 (one :: a) (one :: b) pr | yes y with≡ pr1 | inr th | yes z with≡ pr2 | no with≡ pr3 rewrite pr3 = exFalso (noNotYes th)
+  subLemma3 (one :: a) (one :: b) pr | yes y with≡ pr1 | inr th | yes z with≡ pr2 | yes x with≡ pr3 with inspect (go zero a b)
+  subLemma3 (one :: a) (one :: b) pr | yes y with≡ pr1 | inr th | yes z with≡ pr2 | yes x with≡ pr3 | no with≡ pr4 rewrite pr1 | th | pr2 | pr3 | pr4 | equalityCommutative (yesInjective pr1) = exFalso false
+    where
+      false : False
+      false with applyEquality (mapMaybe canonical) pr3
+      ... | f rewrite th | subLemma5 (incr a) b f = exFalso (noNotYes pr2)
+  subLemma3 (one :: a) (one :: b) pr | yes y with≡ pr1 | inr th | yes z with≡ pr2 | yes x with≡ pr3 | yes w with≡ pr4 rewrite pr4 = exFalso (noNotYes (equalityCommutative pr))
+
+  goIncrOne : (a b : BinNat) → mapMaybe canonical (go one a b) ≡ mapMaybe canonical (go zero a (incr b))
+  goIncrOne [] b rewrite goOneEmpty' b | goZeroIncr b = refl
+  goIncrOne (zero :: a) [] = refl
+  goIncrOne (zero :: a) (zero :: b) = refl
+  goIncrOne (zero :: a) (one :: b) with inspect (go one a b)
+  goIncrOne (zero :: a) (one :: b) | no with≡ pr1 with inspect (go zero a (incr b))
+  goIncrOne (zero :: a) (one :: b) | no with≡ pr1 | no with≡ pr2 rewrite pr1 | pr2 = refl
+  goIncrOne (zero :: a) (one :: b) | no with≡ pr1 | yes x with≡ pr2 with goIncrOne a b
+  ... | f rewrite pr1 | pr2 = exFalso (noNotYes f)
+  goIncrOne (zero :: a) (one :: b) | yes x with≡ pr1 with inspect (go zero a (incr b))
+  goIncrOne (zero :: a) (one :: b) | yes x with≡ pr1 | no with≡ pr2 with goIncrOne a b
+  ... | f rewrite pr1 | pr2 = exFalso (noNotYes (equalityCommutative f))
+  goIncrOne (zero :: a) (one :: b) | yes x with≡ pr1 | yes y with≡ pr2 with goIncrOne a b
+  ... | f rewrite pr1 | pr2 | yesInjective f = refl
+  goIncrOne (one :: a) [] rewrite goEmpty a = refl
+  goIncrOne (one :: a) (zero :: b) = refl
+  goIncrOne (one :: a) (one :: b) with inspect (go one a b)
+  goIncrOne (one :: a) (one :: b) | no with≡ pr with inspect (go zero a (incr b))
+  goIncrOne (one :: a) (one :: b) | no with≡ pr | no with≡ pr2 with goIncrOne a b
+  ... | f rewrite pr | pr2 = refl
+  goIncrOne (one :: a) (one :: b) | no with≡ pr | yes x with≡ pr2 with goIncrOne a b
+  ... | f rewrite pr | pr2 = exFalso (noNotYes f)
+  goIncrOne (one :: a) (one :: b) | yes x with≡ pr with inspect (go zero a (incr b))
+  goIncrOne (one :: a) (one :: b) | yes x with≡ pr | no with≡ pr2 with goIncrOne a b
+  ... | f rewrite pr | pr2 = exFalso (noNotYes (equalityCommutative f))
+  goIncrOne (one :: a) (one :: b) | yes x with≡ pr | yes y with≡ pr2 with goIncrOne a b
+  ... | f rewrite pr | pr2 | yesInjective f = refl
+
+  goIncrIncr : (a b : BinNat) → mapMaybe canonical (go zero (incr a) (incr b)) ≡ mapMaybe canonical (go zero a b)
+  goIncrIncr [] [] = refl
+  goIncrIncr [] (zero :: b) with inspect (go zero [] b)
+  ... | no with≡ pr rewrite goIncrIncr [] b | pr = refl
+  ... | yes y with≡ pr rewrite goIncrIncr [] b | pr | goZeroEmpty' b {y} pr = refl
+  goIncrIncr [] (one :: b) rewrite goZeroIncr b = refl
+  goIncrIncr (zero :: a) [] rewrite goEmpty a = refl
+  goIncrIncr (zero :: a) (zero :: b) = refl
+  goIncrIncr (zero :: a) (one :: b) with inspect (go zero a (incr b))
+  goIncrIncr (zero :: a) (one :: b) | no with≡ pr with inspect (go one a b)
+  goIncrIncr (zero :: a) (one :: b) | no with≡ pr | no with≡ pr2 rewrite pr | pr2 = refl
+  goIncrIncr (zero :: a) (one :: b) | no with≡ pr | yes x with≡ pr2 with goIncrOne a b
+  ... | f rewrite pr | pr2 = exFalso (noNotYes (equalityCommutative f))
+  goIncrIncr (zero :: a) (one :: b) | yes y with≡ pr with inspect (go one a b)
+  goIncrIncr (zero :: a) (one :: b) | yes y with≡ pr | yes z with≡ pr2 with goIncrOne a b
+  ... | f rewrite pr | pr2 = applyEquality (λ i → yes (one :: i)) (equalityCommutative (yesInjective f))
+  goIncrIncr (zero :: a) (one :: b) | yes y with≡ pr | no with≡ pr2 with goIncrOne a b
+  ... | f rewrite pr | pr2 = exFalso (noNotYes f)
+  goIncrIncr (one :: a) [] with goOne a []
+  ... | f with go one (incr a) []
+  goIncrIncr (one :: a) [] | f | no rewrite goEmpty a = exFalso (noNotYes f)
+  goIncrIncr (one :: a) [] | f | yes x rewrite goEmpty a | yesInjective f = refl
+  goIncrIncr (one :: a) (zero :: b) with goOne a b
+  ... | f with go one (incr a) b
+  goIncrIncr (one :: a) (zero :: b) | f | no with go zero a b
+  goIncrIncr (one :: a) (zero :: b) | f | no | no = refl
+  goIncrIncr (one :: a) (zero :: b) | f | yes x with go zero a b
+  goIncrIncr (one :: a) (zero :: b) | f | yes x | yes x₁ rewrite yesInjective f = refl
+  goIncrIncr (one :: a) (one :: b) with goIncrIncr a b
+  ... | f with go zero a b
+  goIncrIncr (one :: a) (one :: b) | f | no with go zero (incr a) (incr b)
+  goIncrIncr (one :: a) (one :: b) | f | no | no = refl
+  goIncrIncr (one :: a) (one :: b) | f | yes x with go zero (incr a) (incr b)
+  goIncrIncr (one :: a) (one :: b) | f | yes x | yes x₁ rewrite yesInjective f = refl
+
+  subtractionConverse : (a b : ℕ) → a <N b → go zero (NToBinNat a) (NToBinNat b) ≡ no
+  subtractionConverse zero (succ b) a<b with NToBinNat b
+  subtractionConverse zero (succ b) a<b | [] = refl
+  subtractionConverse zero (succ b) a<b | zero :: bl = refl
+  subtractionConverse zero (succ b) a<b | one :: bl = goZeroIncr bl
+  subtractionConverse (succ a) (succ b) a<b with inspect (NToBinNat a)
+  subtractionConverse (succ a) (succ b) a<b | [] with≡ pr with inspect (NToBinNat b)
+  subtractionConverse (succ a) (succ b) a<b | [] with≡ pr | [] with≡ pr2 rewrite NToBinNatZero a pr | NToBinNatZero b pr2 = exFalso (TotalOrder.irreflexive ℕTotalOrder a<b)
+  subtractionConverse (succ a) (succ zero) a<b | [] with≡ pr | (zero :: y) with≡ pr2 rewrite NToBinNatZero a pr | pr2 = exFalso (TotalOrder.irreflexive ℕTotalOrder a<b)
+  subtractionConverse (succ a) (succ (succ b)) a<b | [] with≡ pr | (zero :: y) with≡ pr2 with inspect (go zero [] y)
+  ... | no with≡ pr3 rewrite NToBinNatZero a pr | pr2 | pr3 = refl
+  ... | yes t with≡ pr3 with applyEquality canonical pr2
+  ... | g rewrite (goZeroEmpty y pr3) = exFalso (incrNonzero (NToBinNat b) g)
+  subtractionConverse (succ a) (succ b) a<b | [] with≡ pr | (one :: y) with≡ pr2 rewrite NToBinNatZero a pr | pr2 = applyEquality (mapMaybe (one ::_)) (goZeroIncr y)
+  subtractionConverse (succ a) (succ b) a<b | (zero :: y) with≡ pr with inspect (NToBinNat b)
+  subtractionConverse (succ a) (succ b) a<b | (zero :: y) with≡ pr | [] with≡ pr2 rewrite NToBinNatZero b pr2 = exFalso (bad a<b)
+    where
+      bad : {a : ℕ} → succ a <N 1 → False
+      bad {zero} (le zero ())
+      bad {zero} (le (succ x) ())
+      bad {succ a} (le zero ())
+      bad {succ a} (le (succ x) ())
+  subtractionConverse (succ a) (succ b) a<b | (zero :: y) with≡ pr | (zero :: z) with≡ pr2 rewrite pr | pr2 = applyEquality (mapMaybe (zero ::_)) (mapMaybePreservesNo u)
+    where
+      t : go zero (NToBinNat a) (NToBinNat b) ≡ no
+      t = subtractionConverse a b (canRemoveSuccFrom<N a<b)
+      u : go zero (zero :: y) (zero :: z) ≡ no
+      u = transitivity (transitivity {x = _} {go zero (NToBinNat a) (zero :: z)} (applyEquality (λ i → go zero i (zero :: z)) (equalityCommutative pr)) (applyEquality (go zero (NToBinNat a)) (equalityCommutative pr2))) t
+  subtractionConverse (succ a) (succ b) a<b | (zero :: y) with≡ pr | (one :: z) with≡ pr2 with subtractionConverse a (succ b) (le (succ (_<N_.x a<b)) (transitivity (applyEquality succ (transitivity (applyEquality succ (Semiring.commutative ℕSemiring (_<N_.x a<b) a)) (Semiring.commutative ℕSemiring (succ a) (_<N_.x a<b)))) (_<N_.proof a<b)))
+  subtractionConverse (succ a) (succ b) a<b | (zero :: y) with≡ pr | (one :: z) with≡ pr2 | thing=no with subLemma3 (NToBinNat a) (incr (NToBinNat b)) thing=no
+  subtractionConverse (succ a) (succ b) a<b | (zero :: y) with≡ pr | (one :: z) with≡ pr2 | thing=no | inl x = x
+  subtractionConverse (succ a) (succ b) a<b | (zero :: y) with≡ pr | (one :: z) with≡ pr2 | thing=no | inr x rewrite pr | pr2 | mapMaybePreservesNo thing=no = exFalso (noNotYes x)
+  subtractionConverse (succ a) (succ b) a<b | (one :: y) with≡ pr with goIncrIncr (NToBinNat a) (NToBinNat b)
+  ... | f rewrite subtractionConverse a b (canRemoveSuccFrom<N a<b) = mapMaybePreservesNo f
+
+  bad : (b : ℕ) {t : BinNat} → incr (NToBinNat b) ≡ zero :: t → canonical t ≡ [] → False
+  bad b {c} t pr with applyEquality canonical t
+  ... | bl with canonical c
+  bad b {c} t pr | bl | [] = exFalso (incrNonzero (NToBinNat b) bl)
+
+  lemma6 : (a : BinNat) (b : ℕ) → canonical a ≡ [] → NToBinNat b ≡ one :: a → a ≡ []
+  lemma6 [] b pr1 pr2 = refl
+  lemma6 (a :: as) b pr1 pr2 with applyEquality canonical pr2
+  lemma6 (a :: as) b pr1 pr2 | th rewrite pr1 | equalityCommutative (NToBinNatIsCanonical b) | pr2 = exFalso (bad' th)
+    where
+      bad' : one :: a :: as ≡ one :: [] → False
+      bad' ()
+
+  doublingLemma : (y : BinNat) → NToBinNat (2 *N binNatToN y) ≡ canonical (zero :: y)
+  doublingLemma y with inspect (canonical y)
+  doublingLemma y | [] with≡ pr rewrite binNatToNZero' y pr | pr = refl
+  doublingLemma y | (a :: as) with≡ pr with inspect (binNatToN y)
+  doublingLemma y | (a :: as) with≡ pr | zero with≡ pr2 rewrite binNatToNZero y pr2 = exFalso (nonEmptyNotEmpty (equalityCommutative pr))
+  doublingLemma y | (a :: as) with≡ pr | succ bl with≡ pr2 rewrite pr | pr2 | doubleIsBitShift' bl | equalityCommutative pr = applyEquality (zero ::_) (equalityCommutative (transitivity (equalityCommutative (binToBin y)) (applyEquality NToBinNat pr2)))
+
+  doubling : (a : ℕ) {y : BinNat} → (NToBinNat a ≡ zero :: y) → binNatToN y +N (binNatToN y +N 0) ≡ a
+  doubling a {y} pr = NToBinNatInj (binNatToN y +N (binNatToN y +N zero)) a (transitivity (transitivity (equalityCommutative (NToBinNatIsCanonical (binNatToN y +N (binNatToN y +N zero)))) (doublingLemma y)) (applyEquality canonical (equalityCommutative pr)))
+
+  subtraction2 : (a b : ℕ) {t : BinNat} → (NToBinNat a) -B (NToBinNat b) ≡ yes t → (binNatToN t) +N b ≡ a
+  subtraction2 zero zero {t} pr rewrite yesInjective (equalityCommutative pr) = refl
+  subtraction2 zero (succ b) pr with goZeroEmpty (NToBinNat (succ b)) pr
+  ... | t = exFalso (incrNonzero (NToBinNat b) t)
+  subtraction2 (succ a) b {t} pr with inspect (NToBinNat a)
+  subtraction2 (succ a) b {t} pr | [] with≡ pr2 with inspect (NToBinNat b)
+  subtraction2 (succ a) b {t} pr | [] with≡ pr2 | [] with≡ pr3 rewrite pr2 | pr3 | equalityCommutative (yesInjective pr) | NToBinNatZero a pr2 | NToBinNatZero b pr3 = refl
+  subtraction2 (succ a) b {t} pr | [] with≡ pr2 | (zero :: bl) with≡ pr3 with inspect (go zero [] bl)
+  subtraction2 (succ a) b {t} pr | [] with≡ pr2 | (zero :: bl) with≡ pr3 | no with≡ pr4 rewrite pr2 | pr3 | pr4 = exFalso (noNotYes pr)
+  subtraction2 (succ a) b {t} pr | [] with≡ pr2 | (zero :: bl) with≡ pr3 | yes x with≡ pr4 with goZeroEmpty bl pr4
+  subtraction2 (succ a) (succ b) {t} pr | [] with≡ pr2 | (zero :: bl) with≡ pr3 | yes x with≡ pr4 | r with goZeroEmpty' bl pr4
+  ... | s rewrite pr2 | pr3 | pr4 | r | equalityCommutative (yesInjective pr) | NToBinNatZero a pr2 = exFalso (bad b pr3 r)
+  subtraction2 (succ a) b {t} pr | [] with≡ pr2 | (one :: bl) with≡ pr3 with inspect (go zero [] bl)
+  subtraction2 (succ a) b {t} pr | [] with≡ pr2 | (one :: bl) with≡ pr3 | no with≡ pr4 rewrite pr2 | pr3 | pr4 = exFalso (noNotYes pr)
+  subtraction2 (succ a) b {t} pr | [] with≡ pr2 | (one :: bl) with≡ pr3 | yes x with≡ pr4 with goZeroEmpty bl pr4
+  ... | u with goZeroEmpty' bl pr4
+  ... | v rewrite pr2 | pr3 | pr4 | u | NToBinNatZero a pr2 | lemma6 bl b u pr3 | equalityCommutative (yesInjective pr4) | equalityCommutative (yesInjective pr) = ans pr3
+    where
+      z : bl ≡ []
+      z = lemma6 bl b u pr3
+      ans : (NToBinNat b ≡ one :: bl) → b ≡ 1
+      ans pr with applyEquality binNatToN pr
+      ... | th rewrite z = transitivity (equalityCommutative (nToN b)) th
+  subtraction2 (succ a) b pr | (x :: y) with≡ pr2 with inspect (NToBinNat b)
+  subtraction2 (succ a) b pr | (zero :: y) with≡ pr2 | [] with≡ pr3 rewrite NToBinNatZero b pr3 | pr2 | pr3 | equalityCommutative (yesInjective pr) = applyEquality succ (transitivity (Semiring.sumZeroRight ℕSemiring _) (doubling a pr2))
+  subtraction2 (succ a) b pr | (one :: y) with≡ pr2 | [] with≡ pr3 rewrite NToBinNatZero b pr3 | pr2 | pr3 | equalityCommutative (yesInjective pr) = transitivity (Semiring.sumZeroRight ℕSemiring (binNatToN (incr y) +N (binNatToN (incr y) +N zero))) (equalityCommutative (transitivity (equalityCommutative (nToN (succ a))) (applyEquality binNatToN (transitivity (equalityCommutative (NToBinNatSucc a)) (applyEquality incr pr2)))))
+  subtraction2 (succ a) (succ b) {t} pr | (y :: ys) with≡ pr2 | (z :: zs) with≡ pr3 = transitivity (transitivity (Semiring.commutative ℕSemiring (binNatToN t) (succ b)) (applyEquality succ (transitivity (Semiring.commutative ℕSemiring b (binNatToN t)) (applyEquality (_+N b) (equalityCommutative (binNatToNIsCanonical t)))))) (applyEquality succ inter)
+    where
+      inter : binNatToN (canonical t) +N b ≡ a
+      inter with inspect (go zero (NToBinNat a) (NToBinNat b))
+      inter | no with≡ pr4 with goIncrIncr (NToBinNat a) (NToBinNat b)
+      ... | f rewrite pr | pr4 = exFalso (noNotYes (equalityCommutative f))
+      inter | yes x with≡ pr4 with goIncrIncr (NToBinNat a) (NToBinNat b)
+      ... | f with subtraction2 a b {x} pr4
+      ... | g = transitivity (applyEquality (_+N b) (transitivity (applyEquality binNatToN h) (binNatToNIsCanonical x))) g
+        where
+          h : (canonical t) ≡ (canonical x)
+          h rewrite pr | pr4 = yesInjective f
+
+
+  subtraction2' : (a b : ℕ) {t : BinNat} → (NToBinNat a) -B (NToBinNat b) ≡ yes t → b ≤N a
+  subtraction2' a b {t} pr with subtraction2 a b pr
+  ... | f with binNatToN t
+  subtraction2' a b {t} pr | f | zero = inr f
+  subtraction2' a b {t} pr | f | succ g = inl (le g f)
+
+  subtraction2'' : (a b : ℕ) → (pr : b ≤N a) → mapMaybe binNatToN ((NToBinNat a) -B (NToBinNat b)) ≡ yes (subtractionNResult.result (-N pr))
+  subtraction2'' a b pr with -N pr
+  subtraction2'' a b pr | record { result = result ; pr = subPr } with inspect (go zero (NToBinNat a) (NToBinNat b))
+  subtraction2'' a b (inl pr) | record { result = result ; pr = subPr } | no with≡ pr2 with subtraction (NToBinNat a) (NToBinNat b) pr2
+  ... | bl rewrite nToN a | nToN b = exFalso (TotalOrder.irreflexive ℕTotalOrder (TotalOrder.transitive ℕTotalOrder pr bl))
+  subtraction2'' a b (inr pr) | record { result = result ; pr = subPr } | no with≡ pr2 with subtraction (NToBinNat a) (NToBinNat b) pr2
+  ... | bl rewrite nToN a | nToN b | pr = exFalso (TotalOrder.irreflexive ℕTotalOrder bl)
+  subtraction2'' a b pr | record { result = result ; pr = subPr } | yes x with≡ pr2 with subtraction2 a b pr2
+  ... | f rewrite pr2 | Semiring.commutative ℕSemiring (binNatToN x) b = applyEquality yes (canSubtractFromEqualityLeft {b} {binNatToN x} (transitivity f (equalityCommutative subPr)))
diff --git a/Numbers/BinaryNaturals/SubtractionGo.agda b/Numbers/BinaryNaturals/SubtractionGo.agda
new file mode 100644
index 0000000..c6095db
--- /dev/null
+++ b/Numbers/BinaryNaturals/SubtractionGo.agda
@@ -0,0 +1,86 @@
+{-# OPTIONS --warning=error --safe --without-K #-}
+
+open import LogicalFormulae
+open import Lists.Lists
+open import Numbers.Naturals.Naturals
+open import Numbers.BinaryNaturals.Definition
+open import Orders
+open import Semirings.Definition
+open import Maybe
+
+module Numbers.BinaryNaturals.SubtractionGo where
+
+  go : Bit → BinNat → BinNat → Maybe BinNat
+  go zero [] [] = yes []
+  go one [] [] = no
+  go zero [] (zero :: b) = go zero [] b
+  go zero [] (one :: b) = no
+  go one [] (x :: b) = no
+  go zero (zero :: a) [] = yes (zero :: a)
+  go one (zero :: a) [] = mapMaybe (one ::_) (go one a [])
+  go zero (zero :: a) (zero :: b) = mapMaybe (zero ::_) (go zero a b)
+  go one (zero :: a) (zero :: b) = mapMaybe (one ::_) (go one a b)
+  go zero (zero :: a) (one :: b) = mapMaybe (one ::_) (go one a b)
+  go one (zero :: a) (one :: b) = mapMaybe (zero ::_) (go one a b)
+  go zero (one :: a) [] = yes (one :: a)
+  go zero (one :: a) (zero :: b) = mapMaybe (one ::_) (go zero a b)
+  go zero (one :: a) (one :: b) = mapMaybe (zero ::_) (go zero a b)
+  go one (one :: a) [] = yes (zero :: a)
+  go one (one :: a) (zero :: b) = mapMaybe (zero ::_) (go zero a b)
+  go one (one :: a) (one :: b) = mapMaybe (one ::_) (go one a b)
+
+  _-B_ : BinNat → BinNat → Maybe BinNat
+  a -B b = go zero a b
+
+  goEmpty : (a : BinNat) → go zero a [] ≡ yes a
+  goEmpty [] = refl
+  goEmpty (zero :: a) = refl
+  goEmpty (one :: a) = refl
+
+  goOneSelf : (a : BinNat) → go one a a ≡ no
+  goOneSelf [] = refl
+  goOneSelf (zero :: a) rewrite goOneSelf a = refl
+  goOneSelf (one :: a) rewrite goOneSelf a = refl
+
+  goOneEmpty : (b : BinNat) {t : BinNat} → go one [] b ≡ yes t → False
+  goOneEmpty [] {t} ()
+  goOneEmpty (x :: b) {t} ()
+
+  goOneEmpty' : (b : BinNat) → go one [] b ≡ no
+  goOneEmpty' b with inspect (go one [] b)
+  goOneEmpty' b | no with≡ x = x
+  goOneEmpty' b | yes x₁ with≡ x = exFalso (goOneEmpty b x)
+
+  goZeroEmpty : (b : BinNat) {t : BinNat} → go zero [] b ≡ yes t → canonical b ≡ []
+  goZeroEmpty [] {t} = λ _ → refl
+  goZeroEmpty (zero :: b) {t} pr with inspect (canonical b)
+  goZeroEmpty (zero :: b) {t} pr | [] with≡ pr2 rewrite pr2 = refl
+  goZeroEmpty (zero :: b) {t} pr | (x :: r) with≡ pr2 with goZeroEmpty b pr
+  ... | u = exFalso (nonEmptyNotEmpty (transitivity (equalityCommutative pr2) u))
+
+  goZeroEmpty' : (b : BinNat) {t : BinNat} → go zero [] b ≡ yes t → canonical t ≡ []
+  goZeroEmpty' [] {[]} pr = refl
+  goZeroEmpty' (x :: b) {[]} pr = refl
+  goZeroEmpty' (zero :: b) {x₁ :: t} pr = goZeroEmpty' b pr
+
+  goZeroIncr : (b : BinNat) → go zero [] (incr b) ≡ no
+  goZeroIncr [] = refl
+  goZeroIncr (zero :: b) = refl
+  goZeroIncr (one :: b) = goZeroIncr b
+
+  goPreservesCanonicalRightEmpty : (b : BinNat) → go zero [] (canonical b) ≡ go zero [] b
+  goPreservesCanonicalRightEmpty [] = refl
+  goPreservesCanonicalRightEmpty (zero :: b) with inspect (canonical b)
+  goPreservesCanonicalRightEmpty (zero :: b) | [] with≡ x with goPreservesCanonicalRightEmpty b
+  ... | pr2 rewrite x = pr2
+  goPreservesCanonicalRightEmpty (zero :: b) | (x₁ :: y) with≡ x with goPreservesCanonicalRightEmpty b
+  ... | pr2 rewrite x = pr2
+  goPreservesCanonicalRightEmpty (one :: b) = refl
+
+  goZero : (b : BinNat) {t : BinNat} → mapMaybe canonical (go zero [] b) ≡ yes t → t ≡ []
+  goZero b {[]} pr = refl
+  goZero b {x :: t} pr with inspect (go zero [] b)
+  goZero b {x :: t} pr | no with≡ pr2 rewrite pr2 = exFalso (noNotYes pr)
+  goZero b {x :: t} pr | yes x₁ with≡ pr2 with goZeroEmpty b pr2
+  ... | u with applyEquality (mapMaybe canonical) (goPreservesCanonicalRightEmpty b)
+  ... | bl rewrite u | pr = exFalso (nonEmptyNotEmpty (equalityCommutative (yesInjective bl)))
diff --git a/Numbers/BinaryNaturals/SubtractionGoPreservesCanonicalLeft.agda b/Numbers/BinaryNaturals/SubtractionGoPreservesCanonicalLeft.agda
new file mode 100644
index 0000000..df5d279
--- /dev/null
+++ b/Numbers/BinaryNaturals/SubtractionGoPreservesCanonicalLeft.agda
@@ -0,0 +1,179 @@
+{-# OPTIONS --warning=error --safe --without-K #-}
+
+open import LogicalFormulae
+open import Lists.Lists
+open import Numbers.Naturals.Naturals
+open import Numbers.BinaryNaturals.Definition
+open import Maybe
+open import Numbers.BinaryNaturals.SubtractionGo
+
+module Numbers.BinaryNaturals.SubtractionGoPreservesCanonicalLeft where
+
+  goPreservesCanonicalLeftZero : (a b : BinNat) → mapMaybe canonical (go zero a b) ≡ mapMaybe canonical (go zero (canonical a) b)
+  goPreservesCanonicalLeftOne : (a b : BinNat) → mapMaybe canonical (go one a b) ≡ mapMaybe canonical (go one (canonical a) b)
+
+  goPreservesCanonicalLeftZero [] b = refl
+  goPreservesCanonicalLeftZero (zero :: a) [] with inspect (canonical a)
+  goPreservesCanonicalLeftZero (zero :: a) [] | [] with≡ pr rewrite pr = refl
+  goPreservesCanonicalLeftZero (zero :: a) [] | (x :: t) with≡ pr rewrite pr | transitivity (applyEquality canonical (equalityCommutative pr)) (transitivity (equalityCommutative (canonicalIdempotent a)) pr) = refl
+  goPreservesCanonicalLeftZero (zero :: a) (zero :: b) with inspect (canonical a)
+  goPreservesCanonicalLeftZero (zero :: a) (zero :: b) | [] with≡ pr with inspect (go zero a b)
+  goPreservesCanonicalLeftZero (zero :: a) (zero :: b) | [] with≡ pr | no with≡ pr2 rewrite pr | pr2 = transitivity (equalityCommutative (applyEquality (mapMaybe canonical) pr2)) (transitivity (goPreservesCanonicalLeftZero a b) (applyEquality (λ i → mapMaybe canonical (go zero i b)) pr))
+  goPreservesCanonicalLeftZero (zero :: a) (zero :: b) | [] with≡ pr | yes x with≡ pr2 with inspect (canonical x)
+  goPreservesCanonicalLeftZero (zero :: a) (zero :: b) | [] with≡ pr | yes x with≡ pr2 | [] with≡ pr3 rewrite pr | pr2 | pr3 = transitivity (equalityCommutative (transitivity (applyEquality (mapMaybe canonical) pr2) (applyEquality yes pr3))) (transitivity (goPreservesCanonicalLeftZero a b) (applyEquality (λ i → mapMaybe canonical (go zero i b)) pr))
+  goPreservesCanonicalLeftZero (zero :: a) (zero :: b) | [] with≡ pr | yes x with≡ pr2 | (y1 :: ys) with≡ pr3 = exFalso (nonEmptyNotEmpty (goZero b {y1 :: ys} t))
+    where
+      t : mapMaybe canonical (go zero [] b) ≡ yes (y1 :: ys)
+      t = transitivity (transitivity (applyEquality (λ i → mapMaybe canonical (go zero i b)) (equalityCommutative pr)) (transitivity (equalityCommutative (goPreservesCanonicalLeftZero a b)) (applyEquality (mapMaybe canonical) pr2))) (applyEquality yes pr3)
+  goPreservesCanonicalLeftZero (zero :: a) (zero :: b) | (x :: y) with≡ pr with inspect (go zero a b)
+  goPreservesCanonicalLeftZero (zero :: a) (zero :: b) | (x :: y) with≡ pr | no with≡ pr2 with inspect (go zero (x :: y) b)
+  goPreservesCanonicalLeftZero (zero :: a) (zero :: b) | (x :: y) with≡ pr | no with≡ pr2 | no with≡ pr3 rewrite pr | pr2 | pr3 = refl
+  goPreservesCanonicalLeftZero (zero :: a) (zero :: b) | (x :: y) with≡ pr | no with≡ pr2 | yes r with≡ pr3 = exFalso (noNotYes (transitivity (equalityCommutative (transitivity (applyEquality (λ i → mapMaybe canonical (go zero i b)) (equalityCommutative pr)) (transitivity (equalityCommutative (goPreservesCanonicalLeftZero a b)) (applyEquality (mapMaybe canonical) pr2)))) (applyEquality (mapMaybe canonical) pr3)))
+  goPreservesCanonicalLeftZero (zero :: a) (zero :: b) | (x :: y) with≡ pr | yes x1 with≡ pr2 with inspect (go zero (x :: y) b)
+  goPreservesCanonicalLeftZero (zero :: a) (zero :: b) | (x :: y) with≡ pr | yes x1 with≡ pr2 | no with≡ pr3 rewrite equalityCommutative pr = exFalso (noNotYes {b = canonical x1} (transitivity (applyEquality (mapMaybe canonical) (equalityCommutative pr3)) (transitivity (equalityCommutative (goPreservesCanonicalLeftZero a b)) (applyEquality (mapMaybe canonical) pr2))))
+  goPreservesCanonicalLeftZero (zero :: a) (zero :: b) | (x :: y) with≡ pr | yes x1 with≡ pr2 | yes x2 with≡ pr3 with yesInjective {x = canonical x1} {y = canonical x2} (transitivity (transitivity (equalityCommutative (applyEquality (mapMaybe canonical) pr2)) (goPreservesCanonicalLeftZero a b)) (applyEquality (mapMaybe canonical) (transitivity (applyEquality (λ i → go zero i b) pr) pr3)))
+  ... | k rewrite pr | pr2 | pr3 | equalityCommutative pr = applyEquality yes t
+    where
+      t : canonical (zero :: x1) ≡ canonical (zero :: x2)
+      t with inspect (canonical x1)
+      t | [] with≡ pr rewrite pr | equalityCommutative k = refl
+      t | (x :: bl) with≡ pr rewrite pr | equalityCommutative k = refl
+  goPreservesCanonicalLeftZero (zero :: a) (one :: b) with inspect (canonical a)
+  goPreservesCanonicalLeftZero (zero :: a) (one :: b) | [] with≡ x with inspect (go one a b)
+  goPreservesCanonicalLeftZero (zero :: a) (one :: b) | [] with≡ pr | no with≡ pr1 rewrite pr | pr1 = refl
+  goPreservesCanonicalLeftZero (zero :: a) (one :: b) | [] with≡ pr | yes x₂ with≡ pr1 with goPreservesCanonicalLeftOne a b
+  ... | bl rewrite pr1 | pr = exFalso (noNotYes (transitivity (equalityCommutative (applyEquality (mapMaybe canonical) (goOneEmpty' b))) (equalityCommutative bl)))
+  goPreservesCanonicalLeftZero (zero :: a) (one :: b) | (x₁ :: y) with≡ x with inspect (go one a b)
+  goPreservesCanonicalLeftZero (zero :: a) (one :: b) | (r :: rs) with≡ pr1 | no with≡ pr2 with inspect (go one (r :: rs) b)
+  goPreservesCanonicalLeftZero (zero :: a) (one :: b) | (r :: rs) with≡ pr1 | no with≡ pr2 | no with≡ pr3 rewrite pr1 | pr2 | pr3 = refl
+  goPreservesCanonicalLeftZero (zero :: a) (one :: b) | (r :: rs) with≡ pr1 | no with≡ pr2 | yes x with≡ pr3 rewrite pr1 | pr2 | pr3 | equalityCommutative pr1 = exFalso (noNotYes (transitivity (transitivity (equalityCommutative (applyEquality (mapMaybe canonical) pr2)) (goPreservesCanonicalLeftOne a b)) (applyEquality (mapMaybe canonical) pr3)))
+  goPreservesCanonicalLeftZero (zero :: a) (one :: b) | (r :: rs) with≡ pr1 | yes m with≡ pr2 with inspect (go one (r :: rs) b)
+  goPreservesCanonicalLeftZero (zero :: a) (one :: b) | (r :: rs) with≡ pr1 | yes m with≡ pr2 | no with≡ x rewrite pr1 | pr2 | x | equalityCommutative pr1 = exFalso (noNotYes (transitivity (equalityCommutative (transitivity (goPreservesCanonicalLeftOne a b) (applyEquality (mapMaybe canonical) x))) (applyEquality (mapMaybe canonical) pr2)))
+  goPreservesCanonicalLeftZero (zero :: a) (one :: b) | (r :: rs) with≡ pr1 | yes m with≡ pr2 | yes x₁ with≡ x rewrite pr1 | pr2 | x | equalityCommutative pr1 = applyEquality (λ i → yes (one :: i)) (yesInjective (transitivity (transitivity (applyEquality (mapMaybe canonical) (equalityCommutative pr2)) (goPreservesCanonicalLeftOne a b)) (applyEquality (mapMaybe canonical) x)))
+  goPreservesCanonicalLeftZero (one :: a) [] rewrite equalityCommutative (canonicalIdempotent a) = refl
+  goPreservesCanonicalLeftZero (one :: a) (zero :: b) with inspect (canonical a)
+  goPreservesCanonicalLeftZero (one :: a) (zero :: b) | [] with≡ pr with inspect (go zero a b)
+  goPreservesCanonicalLeftZero (one :: a) (zero :: b) | [] with≡ pr | no with≡ pr2 with inspect (go zero [] b)
+  goPreservesCanonicalLeftZero (one :: a) (zero :: b) | [] with≡ pr | no with≡ pr2 | no with≡ pr3 rewrite pr | pr2 | pr3 = refl
+  goPreservesCanonicalLeftZero (one :: a) (zero :: b) | [] with≡ pr | no with≡ pr2 | yes x with≡ pr3 rewrite pr | pr2 | pr3 = exFalso (noNotYes (transitivity (equalityCommutative (transitivity (transitivity (applyEquality (λ i → mapMaybe canonical (go zero i b)) (equalityCommutative pr)) (equalityCommutative (goPreservesCanonicalLeftZero a b))) (applyEquality (mapMaybe canonical) pr2))) (applyEquality (mapMaybe canonical) pr3)))
+  goPreservesCanonicalLeftZero (one :: a) (zero :: b) | [] with≡ pr | yes x with≡ pr2 with inspect (go zero [] b)
+  ... | no with≡ pr3 rewrite pr | pr2 | pr3 = exFalso (noNotYes (transitivity (applyEquality (mapMaybe canonical) (equalityCommutative pr3)) (transitivity (applyEquality (λ i → mapMaybe canonical (go zero i b)) (equalityCommutative pr)) (transitivity (equalityCommutative (goPreservesCanonicalLeftZero a b)) (applyEquality (mapMaybe canonical) pr2)))))
+  ... | yes y with≡ pr3 rewrite pr | pr2 | pr3 = applyEquality (λ i → yes (one :: i)) (yesInjective (transitivity (equalityCommutative (applyEquality (mapMaybe canonical) pr2)) (transitivity (transitivity (goPreservesCanonicalLeftZero a b) (applyEquality (λ i → mapMaybe canonical (go zero i b)) pr)) (applyEquality (mapMaybe canonical) pr3))))
+  goPreservesCanonicalLeftZero (one :: a) (zero :: b) | (x :: y) with≡ pr with inspect (go zero a b)
+  goPreservesCanonicalLeftZero (one :: a) (zero :: b) | (x :: y) with≡ pr | no with≡ pr2 with inspect (go zero (x :: y) b)
+  ... | no with≡ pr3 rewrite pr | pr2 | pr3 = refl
+  ... | yes z with≡ pr3 rewrite pr | pr2 | pr3 | equalityCommutative pr = exFalso (noNotYes (transitivity (equalityCommutative (applyEquality (mapMaybe canonical) pr2)) (transitivity (goPreservesCanonicalLeftZero a b) (applyEquality (mapMaybe canonical) pr3))))
+  goPreservesCanonicalLeftZero (one :: a) (zero :: b) | (x :: y) with≡ pr | yes x₁ with≡ pr2 with inspect (go zero (x :: y) b)
+  ... | no with≡ pr3 rewrite pr | pr2 | pr3 | equalityCommutative pr = exFalso (noNotYes (transitivity (equalityCommutative (transitivity (goPreservesCanonicalLeftZero a b) (applyEquality (mapMaybe canonical) pr3))) (applyEquality (mapMaybe canonical) pr2)))
+  ... | yes z with≡ pr3 rewrite pr | pr2 | pr3 | equalityCommutative pr = applyEquality (λ i → yes (one :: i)) (yesInjective (transitivity (equalityCommutative (transitivity (equalityCommutative (goPreservesCanonicalLeftZero a b)) (applyEquality (mapMaybe canonical) pr2))) (applyEquality (mapMaybe canonical) pr3)))
+  goPreservesCanonicalLeftZero (one :: a) (one :: b) with inspect (canonical a)
+  goPreservesCanonicalLeftZero (one :: a) (one :: b) | [] with≡ x with inspect (go zero a b)
+  goPreservesCanonicalLeftZero (one :: a) (one :: b) | [] with≡ pr | no with≡ pr2 with inspect (go zero [] b)
+  ... | no with≡ pr3 rewrite pr | pr2 | pr3 | equalityCommutative pr = refl
+  ... | yes z with≡ pr3 rewrite pr | pr2 | pr3 | equalityCommutative pr = exFalso (noNotYes (transitivity (applyEquality (mapMaybe canonical) (equalityCommutative pr2)) (transitivity (goPreservesCanonicalLeftZero a b) (applyEquality (mapMaybe canonical) pr3))))
+  goPreservesCanonicalLeftZero (one :: a) (one :: b) | [] with≡ pr | yes y with≡ pr2 with inspect (go zero [] b)
+  ... | no with≡ pr3 rewrite pr | pr2 | pr3 | equalityCommutative pr = exFalso (noNotYes (transitivity (applyEquality (mapMaybe canonical) (equalityCommutative pr3)) (transitivity (equalityCommutative (goPreservesCanonicalLeftZero a b)) (applyEquality (mapMaybe canonical) pr2))))
+  ... | yes z with≡ pr3 rewrite pr | pr2 | pr3 | equalityCommutative pr = applyEquality yes v
+    where
+      t : canonical y ≡ canonical z
+      t = yesInjective (transitivity (transitivity (equalityCommutative (applyEquality (mapMaybe canonical) pr2)) (goPreservesCanonicalLeftZero a b)) (applyEquality (mapMaybe canonical) pr3))
+      v : canonical (zero :: y) ≡ canonical (zero :: z)
+      v with inspect (canonical y)
+      v | [] with≡ pr4 rewrite pr4 | (transitivity (equalityCommutative t) pr4) = refl
+      v | (x :: r) with≡ pr4 rewrite pr4 | transitivity (equalityCommutative t) pr4 = refl
+  goPreservesCanonicalLeftZero (one :: a) (one :: b) | (r :: rs) with≡ x with inspect (go zero a b)
+  goPreservesCanonicalLeftZero (one :: a) (one :: b) | (r :: rs) with≡ pr | no with≡ pr2 with inspect (go zero (r :: rs) b)
+  goPreservesCanonicalLeftZero (one :: a) (one :: b) | (r :: rs) with≡ pr | no with≡ pr2 | no with≡ pr3 rewrite pr | pr2 | pr3 | equalityCommutative pr = refl
+  goPreservesCanonicalLeftZero (one :: a) (one :: b) | (r :: rs) with≡ pr | no with≡ pr2 | yes z with≡ pr3 rewrite pr | pr2 | pr3 | equalityCommutative pr = exFalso (noNotYes (transitivity (equalityCommutative (applyEquality (mapMaybe canonical) pr2)) (transitivity (goPreservesCanonicalLeftZero a b) (applyEquality (mapMaybe canonical) pr3))))
+  goPreservesCanonicalLeftZero (one :: a) (one :: b) | (r :: rs) with≡ pr | yes y with≡ pr2 with inspect (go zero (r :: rs) b)
+  ... | no with≡ pr3 rewrite pr | pr2 | pr3 | equalityCommutative pr = exFalso (noNotYes (transitivity (equalityCommutative (applyEquality (mapMaybe canonical) pr3)) (transitivity (equalityCommutative (goPreservesCanonicalLeftZero a b)) (applyEquality (mapMaybe canonical) pr2))))
+  ... | yes z with≡ pr3 rewrite pr | pr2 | pr3 | equalityCommutative pr = applyEquality yes v
+    where
+      t : canonical y ≡ canonical z
+      t = yesInjective (transitivity (equalityCommutative (transitivity (equalityCommutative (goPreservesCanonicalLeftZero a b)) (applyEquality (mapMaybe canonical) pr2))) (applyEquality (mapMaybe canonical) pr3))
+      v : canonical (zero :: y) ≡ canonical (zero :: z)
+      v with inspect (canonical y)
+      ... | [] with≡ pr4 rewrite pr4 | transitivity (equalityCommutative t) pr4 = refl
+      ... | (r :: rs) with≡ pr4 rewrite pr4 | transitivity (equalityCommutative t) pr4 = refl
+
+  badLemma : (a b : BinNat) {t : BinNat} → go one a b ≡ yes t → canonical a ≡ [] → False
+  badLemma a b pr1 pr2 with applyEquality (mapMaybe canonical) pr1
+  badLemma a b pr1 pr2 | t with goPreservesCanonicalLeftOne a b
+  ... | th rewrite pr2 | t | goOneEmpty' b = noNotYes (equalityCommutative th)
+
+  goPreservesCanonicalLeftOne [] [] = refl
+  goPreservesCanonicalLeftOne [] (x :: b) = refl
+  goPreservesCanonicalLeftOne (zero :: a) [] with inspect (canonical a)
+  goPreservesCanonicalLeftOne (zero :: a) [] | [] with≡ pr with inspect (go one a [])
+  goPreservesCanonicalLeftOne (zero :: a) [] | [] with≡ pr | no with≡ x rewrite pr | x = refl
+  goPreservesCanonicalLeftOne (zero :: a) [] | [] with≡ pr | yes y with≡ x rewrite pr | x = exFalso (noNotYes (transitivity (equalityCommutative (transitivity (goPreservesCanonicalLeftOne a []) (transitivity (applyEquality (λ i → mapMaybe canonical (go one i [])) pr) refl))) (applyEquality (mapMaybe canonical) x)))
+  goPreservesCanonicalLeftOne (zero :: a) [] | (x :: xs) with≡ pr with inspect (go one a [])
+  goPreservesCanonicalLeftOne (zero :: a) [] | (x :: xs) with≡ pr | no with≡ pr2 with inspect (go one (canonical a) [])
+  ... | no with≡ pr3 rewrite pr | pr2 | pr3 | equalityCommutative pr = refl
+  ... | yes z with≡ pr3 rewrite pr | pr2 | pr3 | equalityCommutative pr = exFalso (noNotYes (transitivity (equalityCommutative (applyEquality (mapMaybe canonical) pr2)) (transitivity (goPreservesCanonicalLeftOne a []) (applyEquality (mapMaybe canonical) pr3))))
+  goPreservesCanonicalLeftOne (zero :: a) [] | (x :: xs) with≡ pr | yes y with≡ pr2 with inspect (go one (x :: xs) [])
+  ... | no with≡ pr3 rewrite pr | pr2 | pr3 | equalityCommutative pr = exFalso (noNotYes (transitivity (equalityCommutative (applyEquality (mapMaybe canonical) pr3)) (transitivity (equalityCommutative (goPreservesCanonicalLeftOne a [])) (applyEquality (mapMaybe canonical) pr2))))
+  ... | yes z with≡ pr3 rewrite pr | pr2 | pr3 | equalityCommutative pr = applyEquality (λ i → yes (one :: i)) (yesInjective (transitivity (equalityCommutative (applyEquality (mapMaybe canonical) pr2)) (transitivity (goPreservesCanonicalLeftOne a []) (applyEquality (mapMaybe canonical) pr3))))
+  goPreservesCanonicalLeftOne (one :: a) [] with inspect (canonical a)
+  ... | [] with≡ pr rewrite pr = refl
+  ... | (x :: xs) with≡ pr rewrite pr | equalityCommutative pr = applyEquality yes (transitivity (canonicalAscends' {zero} a λ pr2 → nonEmptyNotEmpty (transitivity (equalityCommutative pr) pr2)) (lemma a))
+    where
+      lemma : (a : BinNat) → canonical (zero :: a) ≡ canonical (zero :: canonical a)
+      lemma [] = refl
+      lemma (zero :: a) with inspect (canonical a)
+      lemma (zero :: a) | [] with≡ pr rewrite pr = refl
+      lemma (zero :: a) | (x :: bl) with≡ pr rewrite pr | equalityCommutative pr | equalityCommutative (canonicalIdempotent a) | pr = refl
+      lemma (one :: a) rewrite equalityCommutative (canonicalIdempotent a) = refl
+  goPreservesCanonicalLeftOne (zero :: as) (zero :: bs) with inspect (go one as bs)
+  goPreservesCanonicalLeftOne (zero :: as) (zero :: bs) | no with≡ pr1 with inspect (canonical as)
+  goPreservesCanonicalLeftOne (zero :: as) (zero :: bs) | no with≡ pr1 | [] with≡ pr2 rewrite pr1 | pr2 = refl
+  goPreservesCanonicalLeftOne (zero :: as) (zero :: bs) | no with≡ pr1 | (a1 :: a) with≡ pr2 with inspect (go one (a1 :: a) bs)
+  ... | no with≡ pr3 rewrite pr1 | pr2 | pr3 = refl
+  ... | yes z with≡ pr3 rewrite pr1 | pr2 | pr3 = exFalso (noNotYes (transitivity (equalityCommutative (applyEquality (mapMaybe canonical) pr1)) (transitivity (transitivity (goPreservesCanonicalLeftOne as bs) (applyEquality (λ i → mapMaybe canonical (go one i bs)) pr2)) (applyEquality (mapMaybe canonical) pr3))))
+  goPreservesCanonicalLeftOne (zero :: as) (zero :: bs) | yes x with≡ pr1 with inspect (canonical as)
+  goPreservesCanonicalLeftOne (zero :: as) (zero :: bs) | yes x with≡ pr1 | [] with≡ pr2 rewrite pr1 | pr2 = exFalso (badLemma as bs pr1 pr2)
+  goPreservesCanonicalLeftOne (zero :: as) (zero :: bs) | yes x with≡ pr1 | (r :: rs) with≡ pr2 with inspect (go one (r :: rs) bs)
+  ... | no with≡ pr3 rewrite pr1 | pr2 | pr3 = exFalso (noNotYes (transitivity (equalityCommutative (applyEquality (mapMaybe canonical) pr3)) (transitivity (equalityCommutative (transitivity (goPreservesCanonicalLeftOne as bs) (applyEquality (λ i → mapMaybe canonical (go one i bs)) pr2))) (applyEquality (mapMaybe canonical) pr1))))
+  ... | yes z with≡ pr3 rewrite pr1 | pr2 | pr3 = applyEquality (λ i → yes (one :: i)) (yesInjective (transitivity (equalityCommutative (applyEquality (mapMaybe canonical) pr1)) (transitivity (transitivity (goPreservesCanonicalLeftOne as bs) (applyEquality (λ i → mapMaybe canonical (go one i bs)) pr2)) (applyEquality (mapMaybe canonical) pr3))))
+  goPreservesCanonicalLeftOne (zero :: as) (one :: bs) with inspect (go one as bs)
+  goPreservesCanonicalLeftOne (zero :: as) (one :: bs) | no with≡ pr with inspect (canonical as)
+  goPreservesCanonicalLeftOne (zero :: as) (one :: bs) | no with≡ pr | [] with≡ pr2 rewrite pr | pr2 = refl
+  goPreservesCanonicalLeftOne (zero :: as) (one :: bs) | no with≡ pr | (r :: rs) with≡ pr2 with inspect (go one (r :: rs) bs)
+  goPreservesCanonicalLeftOne (zero :: as) (one :: bs) | no with≡ pr | (r :: rs) with≡ pr2 | no with≡ pr3 rewrite pr | pr2 | pr3 = refl
+  goPreservesCanonicalLeftOne (zero :: as) (one :: bs) | no with≡ pr | (r :: rs) with≡ pr2 | yes z with≡ pr3 rewrite pr | pr2 | pr3 = exFalso (noNotYes (transitivity (equalityCommutative (applyEquality (mapMaybe canonical) pr)) (transitivity (transitivity (goPreservesCanonicalLeftOne as bs) (applyEquality (λ i → mapMaybe canonical (go one i bs)) pr2)) (applyEquality (mapMaybe canonical) pr3))))
+  goPreservesCanonicalLeftOne (zero :: as) (one :: bs) | yes x₁ with≡ pr with inspect (canonical as)
+  goPreservesCanonicalLeftOne (zero :: as) (one :: bs) | yes x₁ with≡ pr | [] with≡ pr2 rewrite pr | pr2 = exFalso (badLemma as bs pr pr2)
+  goPreservesCanonicalLeftOne (zero :: as) (one :: bs) | yes x₁ with≡ pr | (r :: rs) with≡ pr2 with inspect (go one (r :: rs) bs)
+  goPreservesCanonicalLeftOne (zero :: as) (one :: bs) | yes x₁ with≡ pr | (r :: rs) with≡ pr2 | no with≡ pr3 rewrite pr | pr2 | pr3 = exFalso (noNotYes (transitivity (equalityCommutative (applyEquality (mapMaybe canonical) pr3)) (transitivity (transitivity (applyEquality (λ i → mapMaybe canonical (go one i bs)) (equalityCommutative pr2)) (equalityCommutative (goPreservesCanonicalLeftOne as bs))) (applyEquality (mapMaybe canonical) pr))))
+  goPreservesCanonicalLeftOne (zero :: as) (one :: bs) | yes x with≡ pr | (r :: rs) with≡ pr2 | yes y with≡ pr3 rewrite pr | pr2 | pr3 = applyEquality yes v
+    where
+      t : canonical x ≡ canonical y
+      t = yesInjective (transitivity (equalityCommutative (applyEquality (mapMaybe canonical) pr)) (transitivity (transitivity (goPreservesCanonicalLeftOne as bs) (applyEquality (λ i → mapMaybe canonical (go one i bs)) pr2)) (applyEquality (mapMaybe canonical) pr3)))
+      v : canonical (zero :: x) ≡ canonical (zero :: y)
+      v with inspect (canonical x)
+      ... | [] with≡ pr3 rewrite pr3 | transitivity (equalityCommutative t) pr3 = refl
+      ... | (r :: rs) with≡ pr3 rewrite pr3 | transitivity (equalityCommutative t) pr3 = refl
+  goPreservesCanonicalLeftOne (one :: as) (zero :: bs) with inspect (go zero as bs)
+  goPreservesCanonicalLeftOne (one :: as) (zero :: bs) | no with≡ pr with inspect (go zero (canonical as) bs)
+  goPreservesCanonicalLeftOne (one :: as) (zero :: bs) | no with≡ pr | no with≡ pr2 rewrite pr | pr2 = refl
+  goPreservesCanonicalLeftOne (one :: as) (zero :: bs) | no with≡ pr | yes x with≡ pr2 rewrite pr | pr2 = exFalso (noNotYes (transitivity (applyEquality (mapMaybe canonical) (equalityCommutative pr)) (transitivity (goPreservesCanonicalLeftZero as bs) (applyEquality (mapMaybe canonical) pr2))))
+  goPreservesCanonicalLeftOne (one :: as) (zero :: bs) | yes x with≡ pr with inspect (go zero (canonical as) bs)
+  goPreservesCanonicalLeftOne (one :: as) (zero :: bs) | yes x with≡ pr | yes y with≡ pr2 rewrite pr | pr2 = applyEquality yes v
+    where
+      t : canonical x ≡ canonical y
+      t = yesInjective (transitivity (equalityCommutative (transitivity (equalityCommutative (goPreservesCanonicalLeftZero as bs)) (applyEquality (mapMaybe canonical) pr))) (applyEquality (mapMaybe canonical) pr2))
+      v : canonical (zero :: x) ≡ canonical (zero :: y)
+      v with inspect (canonical x)
+      ... | [] with≡ pr3 rewrite pr3 | transitivity (equalityCommutative t) pr3 = refl
+      ... | (r :: rs) with≡ pr3 rewrite pr3 | transitivity (equalityCommutative t) pr3 = refl
+  goPreservesCanonicalLeftOne (one :: as) (zero :: bs) | yes x with≡ pr | no with≡ pr2 rewrite pr | pr2 = exFalso (noNotYes (transitivity (equalityCommutative (applyEquality (mapMaybe canonical) pr2)) (transitivity (equalityCommutative (goPreservesCanonicalLeftZero as bs)) (applyEquality (mapMaybe canonical) pr))))
+  goPreservesCanonicalLeftOne (one :: as) (one :: bs) with inspect (go one as bs)
+  goPreservesCanonicalLeftOne (one :: as) (one :: bs) | y with≡ pr with inspect (go one (canonical as) bs)
+  goPreservesCanonicalLeftOne (one :: as) (one :: bs) | no with≡ pr | no with≡ pr2 rewrite pr | pr2 = refl
+  goPreservesCanonicalLeftOne (one :: as) (one :: bs) | no with≡ pr | yes x₁ with≡ pr2 rewrite pr | pr2 = exFalso (noNotYes (transitivity (equalityCommutative (applyEquality (mapMaybe canonical) pr)) (transitivity (goPreservesCanonicalLeftOne as bs) (applyEquality (mapMaybe canonical) pr2))))
+  goPreservesCanonicalLeftOne (one :: as) (one :: bs) | yes x₁ with≡ pr | no with≡ pr2 rewrite pr | pr2 = exFalso (noNotYes (transitivity (equalityCommutative (applyEquality (mapMaybe canonical) pr2)) (transitivity (equalityCommutative (goPreservesCanonicalLeftOne as bs)) (applyEquality (mapMaybe canonical) pr))))
+  goPreservesCanonicalLeftOne (one :: as) (one :: bs) | yes x₁ with≡ pr | yes x₂ with≡ pr2 rewrite pr | pr2 = applyEquality (λ i → yes (one :: i)) (yesInjective (transitivity (transitivity (equalityCommutative (applyEquality (mapMaybe canonical) pr)) (goPreservesCanonicalLeftOne as bs)) (applyEquality (mapMaybe canonical) pr2)))
+
+  goPreservesCanonicalLeft : (state : Bit) → (a b : BinNat) → mapMaybe canonical (go state a b) ≡ mapMaybe canonical (go state (canonical a) b)
+  goPreservesCanonicalLeft zero = goPreservesCanonicalLeftZero
+  goPreservesCanonicalLeft one = goPreservesCanonicalLeftOne
diff --git a/Numbers/BinaryNaturals/SubtractionGoPreservesCanonicalRight.agda b/Numbers/BinaryNaturals/SubtractionGoPreservesCanonicalRight.agda
new file mode 100644
index 0000000..1ead2cb
--- /dev/null
+++ b/Numbers/BinaryNaturals/SubtractionGoPreservesCanonicalRight.agda
@@ -0,0 +1,155 @@
+{-# OPTIONS --warning=error --safe --without-K #-}
+
+open import LogicalFormulae
+open import Lists.Lists
+open import Numbers.Naturals.Naturals
+open import Numbers.BinaryNaturals.Definition
+open import Maybe
+open import Numbers.BinaryNaturals.SubtractionGo
+
+module Numbers.BinaryNaturals.SubtractionGoPreservesCanonicalRight where
+
+goPreservesCanonicalRightZero : (a b : BinNat) → mapMaybe canonical (go zero a b) ≡ mapMaybe canonical (go zero a (canonical b))
+goPreservesCanonicalRightOne : (a b : BinNat) → mapMaybe canonical (go one a b) ≡ mapMaybe canonical (go one a (canonical b))
+
+goPreservesCanonicalRightZero [] [] = refl
+goPreservesCanonicalRightZero [] (zero :: b) with inspect (go zero [] b)
+goPreservesCanonicalRightZero [] (zero :: b) | no with≡ pr with inspect (canonical b)
+goPreservesCanonicalRightZero [] (zero :: b) | no with≡ pr | [] with≡ pr2 rewrite pr | pr2 = exFalso (noNotYes (transitivity (equalityCommutative (applyEquality (mapMaybe canonical) pr)) (transitivity (goPreservesCanonicalRightZero [] b) (transitivity (applyEquality (λ i → mapMaybe canonical (go zero [] i)) pr2) refl))))
+goPreservesCanonicalRightZero [] (zero :: b) | no with≡ pr | (x :: y) with≡ pr2 with inspect (go zero [] (x :: y))
+goPreservesCanonicalRightZero [] (zero :: b) | no with≡ pr | (x :: y) with≡ pr2 | no with≡ pr3 rewrite pr | pr2 | pr3 = refl
+goPreservesCanonicalRightZero [] (zero :: b) | no with≡ pr | (x :: y) with≡ pr2 | yes z with≡ pr3 rewrite pr | pr2 | pr3 | equalityCommutative pr2 = exFalso (noNotYes (transitivity (equalityCommutative (applyEquality (mapMaybe canonical) pr)) (transitivity (goPreservesCanonicalRightZero [] b) (applyEquality (mapMaybe canonical) pr3))))
+goPreservesCanonicalRightZero [] (zero :: b) | yes r with≡ pr with inspect (canonical b)
+goPreservesCanonicalRightZero [] (zero :: b) | yes r with≡ pr | [] with≡ pr2 rewrite pr | pr2 = applyEquality yes (goZeroEmpty' b pr)
+goPreservesCanonicalRightZero [] (zero :: b) | yes r with≡ pr | (x :: xs) with≡ pr2 with inspect (go zero [] (x :: xs))
+goPreservesCanonicalRightZero [] (zero :: b) | yes r with≡ pr | (x :: xs) with≡ pr2 | no with≡ pr3 rewrite pr | pr2 | pr3 = exFalso (noNotYes (transitivity (transitivity (equalityCommutative (applyEquality (mapMaybe canonical) pr3)) (transitivity (applyEquality (λ i → mapMaybe canonical (go zero [] i)) (equalityCommutative pr2)) (equalityCommutative (goPreservesCanonicalRightZero [] b)))) (applyEquality (mapMaybe canonical) pr)))
+goPreservesCanonicalRightZero [] (zero :: b) | yes r with≡ pr | (x :: xs) with≡ pr2 | yes x₁ with≡ pr3 rewrite pr | pr2 | pr3 = transitivity (equalityCommutative (applyEquality (mapMaybe canonical) pr)) (transitivity (transitivity (goPreservesCanonicalRightZero [] b) (applyEquality (λ i → mapMaybe canonical (go zero [] i)) pr2)) (applyEquality (mapMaybe canonical) pr3))
+goPreservesCanonicalRightZero [] (one :: b) = refl
+goPreservesCanonicalRightZero (zero :: a) [] = refl
+goPreservesCanonicalRightZero (one :: a) [] = refl
+goPreservesCanonicalRightZero (zero :: a) (zero :: b) with inspect (canonical b)
+goPreservesCanonicalRightZero (zero :: a) (zero :: b) | [] with≡ pr1 with inspect (go zero a b)
+goPreservesCanonicalRightZero (zero :: a) (zero :: b) | [] with≡ pr1 | no with≡ pr2 = exFalso (noNotYes (transitivity (equalityCommutative (applyEquality (mapMaybe canonical) pr2)) (transitivity (goPreservesCanonicalRightZero a b) (transitivity (applyEquality (λ i → mapMaybe canonical (go zero a i)) pr1) (applyEquality (mapMaybe canonical) (goEmpty a))))))
+goPreservesCanonicalRightZero (zero :: a) (zero :: b) | [] with≡ pr1 | yes y with≡ pr2 rewrite pr1 | pr2 = applyEquality yes v
+  where
+    t : canonical y ≡ canonical a
+    t = yesInjective (transitivity (applyEquality (mapMaybe canonical) (equalityCommutative pr2)) (transitivity (goPreservesCanonicalRightZero a b) (transitivity (applyEquality (λ i → mapMaybe canonical (go zero a i)) pr1) (applyEquality (mapMaybe canonical) (goEmpty a)))))
+    v : canonical (zero :: y) ≡ canonical (zero :: a)
+    v with inspect (canonical y)
+    v | [] with≡ pr4 rewrite pr4 | (transitivity (equalityCommutative t) pr4) = refl
+    v | (x :: r) with≡ pr4 rewrite pr4 | transitivity (equalityCommutative t) pr4 = refl
+goPreservesCanonicalRightZero (zero :: a) (zero :: b) | (r :: rs) with≡ pr1 with inspect (go zero a b)
+goPreservesCanonicalRightZero (zero :: a) (zero :: b) | (r :: rs) with≡ pr1 | no with≡ pr2 with inspect (go zero a (r :: rs))
+goPreservesCanonicalRightZero (zero :: a) (zero :: b) | (r :: rs) with≡ pr1 | no with≡ pr2 | no with≡ pr3 rewrite pr1 | pr2 | pr3 = refl
+goPreservesCanonicalRightZero (zero :: a) (zero :: b) | (r :: rs) with≡ pr1 | no with≡ pr2 | yes z with≡ pr3 rewrite pr1 | pr2 | pr3 = exFalso (noNotYes (transitivity (equalityCommutative (applyEquality (mapMaybe canonical) pr2)) (transitivity (transitivity (goPreservesCanonicalRightZero a b) (applyEquality (λ i → mapMaybe canonical (go zero a i)) pr1)) (applyEquality (mapMaybe canonical) pr3))))
+goPreservesCanonicalRightZero (zero :: a) (zero :: b) | (r :: rs) with≡ pr1 | yes y with≡ pr2 with inspect (go zero a (r :: rs))
+goPreservesCanonicalRightZero (zero :: a) (zero :: b) | (r :: rs) with≡ pr1 | yes y with≡ pr2 | no with≡ pr3 rewrite pr1 | pr2 | pr3 = exFalso (noNotYes (transitivity (equalityCommutative (applyEquality (mapMaybe canonical) pr3)) (transitivity (transitivity (applyEquality (λ i → mapMaybe canonical (go zero a i)) (equalityCommutative pr1)) (equalityCommutative (goPreservesCanonicalRightZero a b))) (applyEquality (mapMaybe canonical) pr2))))
+goPreservesCanonicalRightZero (zero :: a) (zero :: b) | (r :: rs) with≡ pr1 | yes y with≡ pr2 | yes z with≡ pr3 rewrite pr1 | pr2 | pr3 = applyEquality yes v
+  where
+    t : canonical y ≡ canonical z
+    t = yesInjective (transitivity (equalityCommutative (applyEquality (mapMaybe canonical) pr2)) (transitivity (goPreservesCanonicalRightZero a b) (transitivity (applyEquality (λ i → mapMaybe canonical (go zero a i)) pr1) (applyEquality (mapMaybe canonical) pr3))))
+    v : canonical (zero :: y) ≡ canonical (zero :: z)
+    v with inspect (canonical y)
+    v | [] with≡ pr4 rewrite pr4 | (transitivity (equalityCommutative t) pr4) = refl
+    v | (x :: r) with≡ pr4 rewrite pr4 | transitivity (equalityCommutative t) pr4 = refl
+goPreservesCanonicalRightZero (zero :: a) (one :: b) with inspect (go one a b)
+goPreservesCanonicalRightZero (zero :: a) (one :: b) | no with≡ x with inspect (go one a (canonical b))
+goPreservesCanonicalRightZero (zero :: a) (one :: b) | no with≡ pr | no with≡ pr2 rewrite pr | pr2 = refl
+goPreservesCanonicalRightZero (zero :: a) (one :: b) | no with≡ pr | yes x with≡ pr2 rewrite pr | pr2 = exFalso (noNotYes (transitivity (equalityCommutative (applyEquality (mapMaybe canonical) pr)) (transitivity (goPreservesCanonicalRightOne a b) (applyEquality (mapMaybe canonical) pr2))))
+goPreservesCanonicalRightZero (zero :: a) (one :: b) | yes r with≡ pr1 with inspect (go one a (canonical b))
+goPreservesCanonicalRightZero (zero :: a) (one :: b) | yes r with≡ pr1 | no with≡ pr2 rewrite pr1 | pr2 = exFalso (noNotYes (transitivity (applyEquality (mapMaybe canonical) (equalityCommutative pr2)) (transitivity (equalityCommutative (goPreservesCanonicalRightOne a b)) (applyEquality (mapMaybe canonical) pr1))))
+goPreservesCanonicalRightZero (zero :: a) (one :: b) | yes r with≡ pr1 | yes s with≡ pr2 rewrite pr1 | pr2 = applyEquality (λ i → yes (one :: i)) (yesInjective (transitivity (equalityCommutative (applyEquality (mapMaybe canonical) pr1)) (transitivity (goPreservesCanonicalRightOne a b) (applyEquality (mapMaybe canonical) pr2))))
+goPreservesCanonicalRightZero (one :: a) (zero :: b) with inspect (go zero a b)
+goPreservesCanonicalRightZero (one :: a) (zero :: b) | no with≡ pr1 with inspect (canonical b)
+goPreservesCanonicalRightZero (one :: a) (zero :: b) | no with≡ pr1 | [] with≡ pr2 rewrite pr1 | pr2 = exFalso (noNotYes (transitivity (equalityCommutative (applyEquality (mapMaybe canonical) pr1)) (transitivity (goPreservesCanonicalRightZero a b) (transitivity (applyEquality (λ i → mapMaybe canonical (go zero a i)) pr2) (applyEquality (mapMaybe canonical) (goEmpty a))))))
+goPreservesCanonicalRightZero (one :: a) (zero :: b) | no with≡ pr1 | (x :: y) with≡ pr2 with inspect (go zero a (x :: y))
+goPreservesCanonicalRightZero (one :: a) (zero :: b) | no with≡ pr1 | (x :: y) with≡ pr2 | no with≡ pr3 rewrite pr1 | pr2 | pr3 = refl
+goPreservesCanonicalRightZero (one :: a) (zero :: b) | no with≡ pr1 | (x :: y) with≡ pr2 | yes z with≡ pr3 rewrite pr1 | pr2 | pr3 = exFalso (noNotYes (transitivity (equalityCommutative (applyEquality (mapMaybe canonical) pr1)) (transitivity (goPreservesCanonicalRightZero a b) (transitivity (applyEquality (λ i → mapMaybe canonical (go zero a i)) pr2) (applyEquality (mapMaybe canonical) pr3)))))
+goPreservesCanonicalRightZero (one :: a) (zero :: b) | yes x with≡ pr1 with inspect (canonical b)
+goPreservesCanonicalRightZero (one :: a) (zero :: b) | yes x with≡ pr1 | [] with≡ pr2 rewrite pr1 | pr2 = applyEquality (λ i → yes (one :: i)) (yesInjective (transitivity (equalityCommutative (applyEquality (mapMaybe canonical) pr1)) (transitivity (goPreservesCanonicalRightZero a b) (transitivity (applyEquality (λ i → mapMaybe canonical (go zero a i)) pr2) (applyEquality (mapMaybe canonical) (goEmpty a))))))
+goPreservesCanonicalRightZero (one :: a) (zero :: b) | yes x with≡ pr1 | (r :: rs) with≡ pr2 with inspect (go zero a (r :: rs))
+goPreservesCanonicalRightZero (one :: a) (zero :: b) | yes x with≡ pr1 | (r :: rs) with≡ pr2 | no with≡ pr3 rewrite pr1 | pr2 | pr3 = exFalso (noNotYes (transitivity (equalityCommutative (applyEquality (mapMaybe canonical) pr3)) (transitivity (transitivity (applyEquality (λ i → mapMaybe canonical (go zero a i)) (equalityCommutative pr2)) (equalityCommutative (goPreservesCanonicalRightZero a b))) (applyEquality (mapMaybe canonical) pr1))))
+goPreservesCanonicalRightZero (one :: a) (zero :: b) | yes x with≡ pr1 | (r :: rs) with≡ pr2 | yes y with≡ pr3 rewrite pr1 | pr2 | pr3 = applyEquality (λ i → yes (one :: i)) (yesInjective (transitivity (equalityCommutative (applyEquality (mapMaybe canonical) pr1)) (transitivity (transitivity (goPreservesCanonicalRightZero a b) (applyEquality (λ i → mapMaybe canonical (go zero a i)) pr2)) (applyEquality (mapMaybe canonical) pr3))))
+goPreservesCanonicalRightZero (one :: a) (one :: b) with inspect (go zero a b)
+goPreservesCanonicalRightZero (one :: a) (one :: b) | no with≡ pr1 with inspect (go zero a (canonical b))
+goPreservesCanonicalRightZero (one :: a) (one :: b) | no with≡ pr1 | no with≡ x rewrite pr1 | x = refl
+goPreservesCanonicalRightZero (one :: a) (one :: b) | no with≡ pr1 | yes x₁ with≡ x rewrite pr1 | x = exFalso (noNotYes (transitivity (applyEquality (mapMaybe canonical) (equalityCommutative pr1)) (transitivity (goPreservesCanonicalRightZero a b) (applyEquality (mapMaybe canonical) x))))
+goPreservesCanonicalRightZero (one :: a) (one :: b) | yes x with≡ pr1 with inspect (go zero a (canonical b))
+goPreservesCanonicalRightZero (one :: a) (one :: b) | yes x with≡ pr1 | no with≡ pr2 rewrite pr1 | pr2 = exFalso (noNotYes (transitivity (applyEquality (mapMaybe canonical) (equalityCommutative pr2)) (transitivity (equalityCommutative (goPreservesCanonicalRightZero a b)) (applyEquality (mapMaybe canonical) pr1))))
+goPreservesCanonicalRightZero (one :: a) (one :: b) | yes x with≡ pr1 | yes y with≡ pr2 rewrite pr1 | pr2 = applyEquality yes v
+  where
+    t : canonical x ≡ canonical y
+    t = yesInjective (transitivity (transitivity (applyEquality (mapMaybe canonical) (equalityCommutative pr1)) (goPreservesCanonicalRightZero a b)) (applyEquality (mapMaybe canonical) pr2))
+    v : canonical (zero :: x) ≡ canonical (zero :: y)
+    v with inspect (canonical x)
+    v | [] with≡ pr4 rewrite pr4 | (transitivity (equalityCommutative t) pr4) = refl
+    v | (x :: r) with≡ pr4 rewrite pr4 | transitivity (equalityCommutative t) pr4 = refl
+
+goPreservesCanonicalRightOne a [] = refl
+goPreservesCanonicalRightOne [] (zero :: b) rewrite goOneEmpty' (canonical (zero :: b)) = refl
+goPreservesCanonicalRightOne (zero :: a) (zero :: b) with inspect (go one a b)
+goPreservesCanonicalRightOne (zero :: a) (zero :: b) | no with≡ pr1 with inspect (canonical b)
+goPreservesCanonicalRightOne (zero :: a) (zero :: b) | no with≡ pr1 | [] with≡ pr2 with inspect (go one a [])
+goPreservesCanonicalRightOne (zero :: a) (zero :: b) | no with≡ pr1 | [] with≡ pr2 | no with≡ pr3 rewrite pr1 | pr2 | pr3 = refl
+goPreservesCanonicalRightOne (zero :: a) (zero :: b) | no with≡ pr1 | [] with≡ pr2 | yes y with≡ pr3 rewrite pr1 | pr2 | pr3 = exFalso (noNotYes (transitivity (equalityCommutative (applyEquality (mapMaybe canonical) pr1)) (transitivity (transitivity (goPreservesCanonicalRightOne a b) (transitivity (applyEquality (λ i → mapMaybe canonical (go one a i)) pr2) refl)) (applyEquality (mapMaybe canonical) pr3))))
+goPreservesCanonicalRightOne (zero :: a) (zero :: b) | no with≡ pr1 | (x :: y) with≡ pr2 with inspect (go one a (x :: y))
+goPreservesCanonicalRightOne (zero :: a) (zero :: b) | no with≡ pr1 | (x :: y) with≡ pr2 | no with≡ pr3 rewrite pr1 | pr2 | pr3 = refl
+goPreservesCanonicalRightOne (zero :: a) (zero :: b) | no with≡ pr1 | (x :: y) with≡ pr2 | yes z with≡ pr3 rewrite pr1 | pr2 | pr3 = exFalso (noNotYes (transitivity (transitivity (equalityCommutative (applyEquality (mapMaybe canonical) pr1)) (transitivity (goPreservesCanonicalRightOne a b) (applyEquality (λ i → mapMaybe canonical (go one a i)) pr2))) (applyEquality (mapMaybe canonical) pr3)))
+goPreservesCanonicalRightOne (zero :: a) (zero :: b) | yes y with≡ pr1 with inspect (canonical b)
+goPreservesCanonicalRightOne (zero :: a) (zero :: b) | yes y with≡ pr1 | [] with≡ pr2 with inspect (go one a [])
+goPreservesCanonicalRightOne (zero :: a) (zero :: b) | yes y with≡ pr1 | [] with≡ pr2 | no with≡ pr3 rewrite pr1 | pr2 | pr3 = exFalso (noNotYes (transitivity (transitivity (equalityCommutative (applyEquality (mapMaybe canonical) pr3)) (transitivity (applyEquality (λ i → mapMaybe canonical (go one a i)) (equalityCommutative pr2)) (equalityCommutative (goPreservesCanonicalRightOne a b)))) (applyEquality (mapMaybe canonical) pr1)))
+goPreservesCanonicalRightOne (zero :: a) (zero :: b) | yes y with≡ pr1 | [] with≡ pr2 | yes z with≡ pr3 rewrite pr1 | pr2 | pr3 = applyEquality (λ i → yes (one :: i)) (yesInjective (transitivity (equalityCommutative (applyEquality (mapMaybe canonical) pr1)) (transitivity (transitivity (goPreservesCanonicalRightOne a b) (applyEquality (λ i → mapMaybe canonical (go one a i)) pr2)) (applyEquality (mapMaybe canonical) pr3))))
+goPreservesCanonicalRightOne (zero :: a) (zero :: b) | yes y with≡ pr1 | (r :: rs) with≡ pr2 with inspect (go one a (r :: rs))
+goPreservesCanonicalRightOne (zero :: a) (zero :: b) | yes y with≡ pr1 | (r :: rs) with≡ pr2 | no with≡ pr3 rewrite pr1 | pr2 | pr3 = exFalso (noNotYes (transitivity (equalityCommutative (applyEquality (mapMaybe canonical) pr3)) (transitivity (applyEquality (λ i → mapMaybe canonical (go one a i)) (equalityCommutative pr2)) (transitivity (equalityCommutative (goPreservesCanonicalRightOne a b)) (applyEquality (mapMaybe canonical) pr1)))))
+goPreservesCanonicalRightOne (zero :: a) (zero :: b) | yes y with≡ pr1 | (r :: rs) with≡ pr2 | yes z with≡ pr3 rewrite pr1 | pr2 | pr3 = applyEquality (λ i → yes (one :: i)) (yesInjective (transitivity (equalityCommutative (applyEquality (mapMaybe canonical) pr1)) (transitivity (transitivity (goPreservesCanonicalRightOne a b) (applyEquality (λ i → mapMaybe canonical (go one a i)) pr2)) (applyEquality (mapMaybe canonical) pr3))))
+goPreservesCanonicalRightOne (one :: a) (zero :: b) with inspect (go zero a b)
+goPreservesCanonicalRightOne (one :: a) (zero :: b) | no with≡ pr1 with inspect (canonical b)
+goPreservesCanonicalRightOne (one :: a) (zero :: b) | no with≡ pr1 | [] with≡ pr2 rewrite pr1 | pr2 = exFalso (noNotYes (transitivity (equalityCommutative (applyEquality (mapMaybe canonical) pr1)) (transitivity (goPreservesCanonicalRightZero a b) (transitivity (applyEquality (λ i → mapMaybe canonical (go zero a i)) pr2) (applyEquality (mapMaybe canonical) (goEmpty a))))))
+goPreservesCanonicalRightOne (one :: a) (zero :: b) | no with≡ pr1 | (r :: rs) with≡ pr2 with inspect (go zero a (r :: rs))
+goPreservesCanonicalRightOne (one :: a) (zero :: b) | no with≡ pr1 | (r :: rs) with≡ pr2 | no with≡ pr3 rewrite pr1 | pr2 | pr3 = refl
+goPreservesCanonicalRightOne (one :: a) (zero :: b) | no with≡ pr1 | (r :: rs) with≡ pr2 | yes y with≡ pr3 rewrite pr1 | pr2 | pr3 = exFalso (noNotYes (transitivity (equalityCommutative (applyEquality (mapMaybe canonical) pr1)) (transitivity (transitivity (goPreservesCanonicalRightZero a b) (applyEquality (λ i → mapMaybe canonical (go zero a i)) pr2)) (applyEquality (mapMaybe canonical) pr3))))
+goPreservesCanonicalRightOne (one :: a) (zero :: b) | yes y with≡ pr1 with inspect (canonical b)
+goPreservesCanonicalRightOne (one :: a) (zero :: b) | yes y with≡ pr1 | [] with≡ pr2 rewrite pr1 | pr2 = applyEquality yes v
+  where
+    t : canonical y ≡ canonical a
+    t = yesInjective (transitivity (equalityCommutative (applyEquality (mapMaybe canonical) pr1)) (transitivity (goPreservesCanonicalRightZero a b) (transitivity (applyEquality (λ i → mapMaybe canonical (go zero a i)) pr2) (applyEquality (mapMaybe canonical) (goEmpty a)))))
+    v : canonical (zero :: y) ≡ canonical (zero :: a)
+    v with inspect (canonical y)
+    v | [] with≡ pr4 rewrite pr4 | (transitivity (equalityCommutative t) pr4) = refl
+    v | (x :: r) with≡ pr4 rewrite pr4 | transitivity (equalityCommutative t) pr4 = refl
+goPreservesCanonicalRightOne (one :: a) (zero :: b) | yes y with≡ pr1 | (r :: rs) with≡ pr2 with inspect (go zero a (r :: rs))
+goPreservesCanonicalRightOne (one :: a) (zero :: b) | yes y with≡ pr1 | (r :: rs) with≡ pr2 | no with≡ pr3 rewrite pr1 | pr2 | pr3 = exFalso (noNotYes (transitivity (equalityCommutative (transitivity (transitivity (goPreservesCanonicalRightZero a b) (applyEquality (λ i → mapMaybe canonical (go zero a i)) pr2)) (applyEquality (mapMaybe canonical) pr3))) (applyEquality (mapMaybe canonical) pr1)))
+goPreservesCanonicalRightOne (one :: a) (zero :: b) | yes y with≡ pr1 | (r :: rs) with≡ pr2 | yes z with≡ pr3 rewrite pr1 | pr2 | pr3 = applyEquality yes v
+  where
+    t : canonical y ≡ canonical z
+    t = yesInjective (transitivity (equalityCommutative (applyEquality (mapMaybe canonical) pr1)) (transitivity (goPreservesCanonicalRightZero a b) (transitivity (applyEquality (λ i → mapMaybe canonical (go zero a i)) pr2) (applyEquality (mapMaybe canonical) pr3))))
+    v : canonical (zero :: y) ≡ canonical (zero :: z)
+    v with inspect (canonical y)
+    v | [] with≡ pr4 rewrite pr4 | (transitivity (equalityCommutative t) pr4) = refl
+    v | (x :: r) with≡ pr4 rewrite pr4 | transitivity (equalityCommutative t) pr4 = refl
+goPreservesCanonicalRightOne [] (one :: b) = refl
+goPreservesCanonicalRightOne (zero :: a) (one :: b) with inspect (go one a b)
+goPreservesCanonicalRightOne (zero :: a) (one :: b) | no with≡ pr1 with inspect (go one a (canonical b))
+goPreservesCanonicalRightOne (zero :: a) (one :: b) | no with≡ pr1 | no with≡ pr2 rewrite pr1 | pr2 = refl
+goPreservesCanonicalRightOne (zero :: a) (one :: b) | no with≡ pr1 | yes y with≡ pr2 rewrite pr1 | pr2 = exFalso (noNotYes (transitivity (equalityCommutative (applyEquality (mapMaybe canonical) pr1)) (transitivity (goPreservesCanonicalRightOne a b) (applyEquality (mapMaybe canonical) pr2))))
+goPreservesCanonicalRightOne (zero :: a) (one :: b) | yes y with≡ pr1 with inspect (go one a (canonical b))
+goPreservesCanonicalRightOne (zero :: a) (one :: b) | yes y with≡ pr1 | no with≡ pr2 rewrite pr1 | pr2 = exFalso (noNotYes (transitivity (equalityCommutative (applyEquality (mapMaybe canonical) pr2)) (transitivity (equalityCommutative (goPreservesCanonicalRightOne a b)) (applyEquality (mapMaybe canonical) pr1))))
+goPreservesCanonicalRightOne (zero :: a) (one :: b) | yes y with≡ pr1 | yes z with≡ pr2 rewrite pr1 | pr2 = applyEquality yes v
+  where
+    t : canonical y ≡ canonical z
+    t = yesInjective (transitivity (transitivity (applyEquality (mapMaybe canonical) (equalityCommutative pr1)) (goPreservesCanonicalRightOne a b)) (applyEquality (mapMaybe canonical) pr2))
+    v : canonical (zero :: y) ≡ canonical (zero :: z)
+    v with inspect (canonical y)
+    v | [] with≡ pr4 rewrite pr4 | (transitivity (equalityCommutative t) pr4) = refl
+    v | (x :: r) with≡ pr4 rewrite pr4 | transitivity (equalityCommutative t) pr4 = refl
+goPreservesCanonicalRightOne (one :: a) (one :: b) with inspect (go one a b)
+goPreservesCanonicalRightOne (one :: a) (one :: b) | no with≡ pr1 with inspect (go one a (canonical b))
+goPreservesCanonicalRightOne (one :: a) (one :: b) | no with≡ pr1 | no with≡ pr2 rewrite pr1 | pr2 = refl
+goPreservesCanonicalRightOne (one :: a) (one :: b) | no with≡ pr1 | yes y with≡ pr2 rewrite pr1 | pr2 = exFalso (noNotYes (transitivity (equalityCommutative (applyEquality (mapMaybe canonical) pr1)) (transitivity (goPreservesCanonicalRightOne a b) (applyEquality (mapMaybe canonical) pr2))))
+goPreservesCanonicalRightOne (one :: a) (one :: b) | yes y with≡ pr1 with inspect (go one a (canonical b))
+goPreservesCanonicalRightOne (one :: a) (one :: b) | yes y with≡ pr1 | yes z with≡ pr2 rewrite pr1 | pr2 = applyEquality (λ i → yes (one :: i)) (yesInjective (transitivity (transitivity (applyEquality (mapMaybe canonical) (equalityCommutative pr1)) (goPreservesCanonicalRightOne a b) ) (applyEquality (mapMaybe canonical) pr2)))
+goPreservesCanonicalRightOne (one :: a) (one :: b) | yes y with≡ pr1 | no with≡ pr2 rewrite pr1 | pr2 = exFalso (noNotYes (transitivity (equalityCommutative (applyEquality (mapMaybe canonical) pr2)) (transitivity (equalityCommutative (goPreservesCanonicalRightOne a b)) (applyEquality (mapMaybe canonical) pr1))))
+
+goPreservesCanonicalRight : (state : Bit) → (a b : BinNat) → mapMaybe canonical (go state a b) ≡ mapMaybe canonical (go state a (canonical b))
+goPreservesCanonicalRight zero = goPreservesCanonicalRightZero
+goPreservesCanonicalRight one = goPreservesCanonicalRightOne