From cfd9787bb88bd8ddd47fb8bdf5b2318238f45040 Mon Sep 17 00:00:00 2001
From: Patrick Stevens <smaug451@gmail.com>
Date: Wed, 4 Dec 2019 19:53:34 +0000
Subject: [PATCH] Problem 1 of Project Euler (#85)

---
 Decidable/Relations.agda                   |  37 ++
 Decidable/Sets.agda                        |  10 +
 DecidableSet.agda                          |  10 -
 Everything/Safe.agda                       |   3 +-
 Everything/WithK.agda                      |   2 +
 Groups/FreeGroups.agda                     |   4 +-
 LogicalFormulae.agda                       |   4 +
 Numbers/BinaryNaturals/Definition.agda     | 564 ++++++++++-----------
 Numbers/BinaryNaturals/Multiplication.agda | 304 +++++------
 ProjectEuler/Problem1.agda                 |  35 ++
 10 files changed, 526 insertions(+), 447 deletions(-)
 create mode 100644 Decidable/Relations.agda
 create mode 100644 Decidable/Sets.agda
 delete mode 100644 DecidableSet.agda
 create mode 100644 ProjectEuler/Problem1.agda

diff --git a/Decidable/Relations.agda b/Decidable/Relations.agda
new file mode 100644
index 0000000..cbd245e
--- /dev/null
+++ b/Decidable/Relations.agda
@@ -0,0 +1,37 @@
+{-# OPTIONS --safe --warning=error --without-K #-}
+
+open import LogicalFormulae
+open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
+
+module Decidable.Relations where
+
+DecidableRelation : {a b : _} {A : Set a} (f : A → Set b) → Set (a ⊔ b)
+DecidableRelation {A = A} f = (x : A) → (f x) || (f x → False)
+
+orDecidable : {a b c : _} {A : Set a} {f : A → Set b} {g : A → Set c} → DecidableRelation f → DecidableRelation g → DecidableRelation (λ x → (f x) || (g x))
+orDecidable fDec gDec x with fDec x
+orDecidable fDec gDec x | inl fx = inl (inl fx)
+orDecidable fDec gDec x | inr !fx with gDec x
+orDecidable fDec gDec x | inr !fx | inl gx = inl (inr gx)
+orDecidable {f = f} {g} fDec gDec x | inr !fx | inr !gx = inr t
+  where
+    t : (f x || g x) → False
+    t (inl x) = !fx x
+    t (inr x) = !gx x
+
+andDecidable : {a b c : _} {A : Set a} {f : A → Set b} {g : A → Set c} → DecidableRelation f → DecidableRelation g → DecidableRelation (λ x → (f x) && (g x))
+andDecidable fDec gDec x with fDec x
+andDecidable fDec gDec x | inl fx with gDec x
+andDecidable fDec gDec x | inl fx | inl gx = inl (fx ,, gx)
+andDecidable fDec gDec x | inl fx | inr !gx = inr (λ x → !gx (_&&_.snd x))
+andDecidable fDec gDec x | inr !fx = inr (λ x → !fx (_&&_.fst x))
+
+notDecidable : {a b : _} {A : Set a} {f : A → Set b} → DecidableRelation f → DecidableRelation (λ x → (f x) → False)
+notDecidable fDec x with fDec x
+notDecidable fDec x | inl fx = inr (λ x → x fx)
+notDecidable fDec x | inr !fx = inl !fx
+
+doubleNegation : {a b : _} {A : Set a} {f : A → Set b} → DecidableRelation f → (x : A) → (((f x) → False) → False) → f x
+doubleNegation fDec x with fDec x
+doubleNegation fDec x | inl fx = λ _ → fx
+doubleNegation fDec x | inr !fx = λ p → exFalso (p !fx)
diff --git a/Decidable/Sets.agda b/Decidable/Sets.agda
new file mode 100644
index 0000000..b8b0991
--- /dev/null
+++ b/Decidable/Sets.agda
@@ -0,0 +1,10 @@
+{-# OPTIONS --safe --warning=error --without-K #-}
+
+open import LogicalFormulae
+open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
+
+module Decidable.Sets where
+
+record DecidableSet {a : _} (A : Set a) : Set a where
+  field
+    eq : (a b : A) → ((a ≡ b) || ((a ≡ b) → False))
diff --git a/DecidableSet.agda b/DecidableSet.agda
deleted file mode 100644
index e652af0..0000000
--- a/DecidableSet.agda
+++ /dev/null
@@ -1,10 +0,0 @@
-{-# OPTIONS --safe --warning=error --without-K #-}
-
-open import LogicalFormulae
-open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
-
-module DecidableSet where
-
-  record DecidableSet {a : _} (A : Set a) : Set a where
-    field
-      eq : (a b : A) → ((a ≡ b) || ((a ≡ b) → False))
diff --git a/Everything/Safe.agda b/Everything/Safe.agda
index 43f9d2a..8d418ee 100644
--- a/Everything/Safe.agda
+++ b/Everything/Safe.agda
@@ -79,7 +79,8 @@ open import Setoids.Functions.Extension
 open import Sets.Cardinality
 open import Sets.FinSet
 
-open import DecidableSet
+open import Decidable.Sets
+open import Decidable.Relations
 
 open import Vectors
 open import Vectors.VectorSpace
diff --git a/Everything/WithK.agda b/Everything/WithK.agda
index 169c2c0..dca4934 100644
--- a/Everything/WithK.agda
+++ b/Everything/WithK.agda
@@ -27,4 +27,6 @@ open import Groups.LectureNotes.Lecture1
 open import LectureNotes.NumbersAndSets.Lecture1
 open import LectureNotes.Groups.Lecture1
 
+open import ProjectEuler.Problem1
+
 module Everything.WithK where
diff --git a/Groups/FreeGroups.agda b/Groups/FreeGroups.agda
index a31c226..4807c4a 100644
--- a/Groups/FreeGroups.agda
+++ b/Groups/FreeGroups.agda
@@ -11,7 +11,7 @@ open import Numbers.Naturals.WithK
 open import Sets.FinSet
 open import Groups.Definition
 open import Groups.SymmetricGroups.Definition
-open import DecidableSet
+open import Decidable.Sets
 
 module Groups.FreeGroups where
 
@@ -107,7 +107,7 @@ badPrepend' {decA = decA} {x} (wordEnding pr x₁) | inr pr2 = pr2 refl
 freeGroupGenerators : {a : _} (A : Set a) (decA : DecidableSet A) (w : FreeGroupGenerators A) → SymmetryGroupElements (reflSetoid (ReducedWord decA))
 freeGroupGenerators A decA (χ x) = sym {f = f} bij
   where
-    open DecidableSet.DecidableSet decA
+    open DecidableSet decA
     f : ReducedWord decA → ReducedWord decA
     f empty = prependLetter (ofLetter x) empty (wordEmpty refl)
     f (prependLetter (ofLetter startLetter) w pr) = prependLetter (ofLetter x) (prependLetter (ofLetter startLetter) w pr) (wordEnding (succIsPositive _) ans)
diff --git a/LogicalFormulae.agda b/LogicalFormulae.agda
index 87ab1b2..30642eb 100644
--- a/LogicalFormulae.agda
+++ b/LogicalFormulae.agda
@@ -94,6 +94,10 @@ boolAnd : Bool → Bool → Bool
 boolAnd BoolTrue y = y
 boolAnd BoolFalse y = BoolFalse
 
+boolOr : Bool → Bool → Bool
+boolOr BoolTrue y = BoolTrue
+boolOr BoolFalse y = y
+
 typeCast : {a : _} {A : Set a} {B : Set a} (el : A) (pr : A ≡ B) → B
 typeCast {a} {A} {.A} elt refl = elt
 
diff --git a/Numbers/BinaryNaturals/Definition.agda b/Numbers/BinaryNaturals/Definition.agda
index 0f2c6cb..8bcf49e 100644
--- a/Numbers/BinaryNaturals/Definition.agda
+++ b/Numbers/BinaryNaturals/Definition.agda
@@ -12,343 +12,343 @@ open import Orders
 
 module Numbers.BinaryNaturals.Definition where
 
-  data Bit : Set where
-    zero : Bit
-    one : Bit
+data Bit : Set where
+  zero : Bit
+  one : Bit
 
-  BinNat : Set
-  BinNat = List Bit
+BinNat : Set
+BinNat = List Bit
 
-  ::Inj : {xs ys : BinNat} {i : Bit} → i :: xs ≡ i :: ys → xs ≡ ys
-  ::Inj {i = zero} refl = refl
-  ::Inj {i = one} refl = refl
+::Inj : {xs ys : BinNat} {i : Bit} → i :: xs ≡ i :: ys → xs ≡ ys
+::Inj {i = zero} refl = refl
+::Inj {i = one} refl = refl
 
-  nonEmptyNotEmpty : {a : _} {A : Set a} {l1 : List A} {i : A} → i :: l1 ≡ [] → False
-  nonEmptyNotEmpty {l1 = l1} {i} ()
+nonEmptyNotEmpty : {a : _} {A : Set a} {l1 : List A} {i : A} → i :: l1 ≡ [] → False
+nonEmptyNotEmpty {l1 = l1} {i} ()
 
 -- TODO - maybe we should do the floating-point style of assuming there's a leading bit and not storing it.
 -- That way, everything is already canonical.
 
-  canonical : BinNat → BinNat
-  canonical [] = []
-  canonical (zero :: n) with canonical n
-  canonical (zero :: n) | [] = []
-  canonical (zero :: n) | x :: bl = zero :: x :: bl
-  canonical (one :: n) = one :: canonical n
+canonical : BinNat → BinNat
+canonical [] = []
+canonical (zero :: n) with canonical n
+canonical (zero :: n) | [] = []
+canonical (zero :: n) | x :: bl = zero :: x :: bl
+canonical (one :: n) = one :: canonical n
 
-  Canonicalised : Set
-  Canonicalised = Sg BinNat (λ i → canonical i ≡ i)
+Canonicalised : Set
+Canonicalised = Sg BinNat (λ i → canonical i ≡ i)
 
-  binNatToN : BinNat → ℕ
-  binNatToN [] = 0
-  binNatToN (zero :: b) = 2 *N binNatToN b
-  binNatToN (one :: b) = 1 +N (2 *N binNatToN b)
+binNatToN : BinNat → ℕ
+binNatToN [] = 0
+binNatToN (zero :: b) = 2 *N binNatToN b
+binNatToN (one :: b) = 1 +N (2 *N binNatToN b)
 
-  incr : BinNat → BinNat
-  incr [] = one :: []
-  incr (zero :: n) = one :: n
-  incr (one :: n) = zero :: (incr n)
+incr : BinNat → BinNat
+incr [] = one :: []
+incr (zero :: n) = one :: n
+incr (one :: n) = zero :: (incr n)
 
-  incrNonzero : (x : BinNat) → canonical (incr x) ≡ [] → False
+incrNonzero : (x : BinNat) → canonical (incr x) ≡ [] → False
 
-  incrPreservesCanonical : (x : BinNat) → (canonical x ≡ x) → canonical (incr x) ≡ incr x
-  incrPreservesCanonical [] pr = refl
-  incrPreservesCanonical (zero :: xs) pr with canonical xs
-  incrPreservesCanonical (zero :: xs) pr | x :: t = applyEquality (one ::_) (::Inj pr)
-  incrPreservesCanonical (one :: xs) pr with inspect (canonical (incr xs))
-  incrPreservesCanonical (one :: xs) pr | [] with≡ x = exFalso (incrNonzero xs x)
-  incrPreservesCanonical (one :: xs) pr | (x₁ :: y) with≡ x rewrite x = applyEquality (zero ::_) (transitivity (equalityCommutative x) (incrPreservesCanonical xs (::Inj pr)))
+incrPreservesCanonical : (x : BinNat) → (canonical x ≡ x) → canonical (incr x) ≡ incr x
+incrPreservesCanonical [] pr = refl
+incrPreservesCanonical (zero :: xs) pr with canonical xs
+incrPreservesCanonical (zero :: xs) pr | x :: t = applyEquality (one ::_) (::Inj pr)
+incrPreservesCanonical (one :: xs) pr with inspect (canonical (incr xs))
+incrPreservesCanonical (one :: xs) pr | [] with≡ x = exFalso (incrNonzero xs x)
+incrPreservesCanonical (one :: xs) pr | (x₁ :: y) with≡ x rewrite x = applyEquality (zero ::_) (transitivity (equalityCommutative x) (incrPreservesCanonical xs (::Inj pr)))
 
-  incrPreservesCanonical' : (x : BinNat) → canonical (incr x) ≡ incr (canonical x)
+incrPreservesCanonical' : (x : BinNat) → canonical (incr x) ≡ incr (canonical x)
 
-  incrC : Canonicalised → Canonicalised
-  incrC (a , b) = incr a , incrPreservesCanonical a b
+incrC : Canonicalised → Canonicalised
+incrC (a , b) = incr a , incrPreservesCanonical a b
 
-  NToBinNat : ℕ → BinNat
-  NToBinNat zero = []
-  NToBinNat (succ n) with NToBinNat n
-  NToBinNat (succ n) | t = incr t
+NToBinNat : ℕ → BinNat
+NToBinNat zero = []
+NToBinNat (succ n) with NToBinNat n
+NToBinNat (succ n) | t = incr t
 
-  NToBinNatC : ℕ → Canonicalised
-  NToBinNatC zero = [] , refl
-  NToBinNatC (succ n) = incrC (NToBinNatC n)
+NToBinNatC : ℕ → Canonicalised
+NToBinNatC zero = [] , refl
+NToBinNatC (succ n) = incrC (NToBinNatC n)
 
-  incrInj : {x y : BinNat} → incr x ≡ incr y → canonical x ≡ canonical y
+incrInj : {x y : BinNat} → incr x ≡ incr y → canonical x ≡ canonical y
 
-  incrNonzero' : (x : BinNat) → (incr x) ≡ [] → False
-  incrNonzero' (zero :: xs) ()
-  incrNonzero' (one :: xs) ()
+incrNonzero' : (x : BinNat) → (incr x) ≡ [] → False
+incrNonzero' (zero :: xs) ()
+incrNonzero' (one :: xs) ()
 
-  canonicalRespectsIncr' : {x y : BinNat} → canonical (incr x) ≡ canonical (incr y) → canonical x ≡ canonical y
+canonicalRespectsIncr' : {x y : BinNat} → canonical (incr x) ≡ canonical (incr y) → canonical x ≡ canonical y
 
-  binNatToNSucc : (n : BinNat) → binNatToN (incr n) ≡ succ (binNatToN n)
-  NToBinNatSucc : (n : ℕ) → incr (NToBinNat n) ≡ NToBinNat (succ n)
+binNatToNSucc : (n : BinNat) → binNatToN (incr n) ≡ succ (binNatToN n)
+NToBinNatSucc : (n : ℕ) → incr (NToBinNat n) ≡ NToBinNat (succ n)
 
-  binNatToNZero : (x : BinNat) → binNatToN x ≡ 0 → canonical x ≡ []
-  binNatToNZero' : (x : BinNat) → canonical x ≡ [] → binNatToN x ≡ 0
+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)
+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) → 0 <N binNatToN a → i :: canonical a ≡ canonical (i :: a)
 
-  canonicalAscends' : {i : Bit} → (a : BinNat) → (canonical a ≡ [] → False) → i :: canonical a ≡ canonical (i :: a)
-  canonicalAscends' {i} a pr = canonicalAscends {i} a (t a pr)
-    where
-      t : (a : BinNat) → (canonical a ≡ [] → False) → 0 <N binNatToN a
-      t a pr with TotalOrder.totality ℕTotalOrder 0 (binNatToN a)
-      t a pr | inl (inl x) = x
-      t a pr | inr x = exFalso (pr (binNatToNZero a (equalityCommutative x)))
+canonicalAscends' : {i : Bit} → (a : BinNat) → (canonical a ≡ [] → False) → i :: canonical a ≡ canonical (i :: a)
+canonicalAscends' {i} a pr = canonicalAscends {i} a (t a pr)
+  where
+    t : (a : BinNat) → (canonical a ≡ [] → False) → 0 <N binNatToN a
+    t a pr with TotalOrder.totality ℕTotalOrder 0 (binNatToN a)
+    t a pr | inl (inl x) = x
+    t a pr | inr x = exFalso (pr (binNatToNZero a (equalityCommutative x)))
 
-  canonicalIdempotent : (a : BinNat) → canonical a ≡ canonical (canonical a)
-  canonicalIdempotent [] = refl
-  canonicalIdempotent (zero :: a) with inspect (canonical a)
-  canonicalIdempotent (zero :: a) | [] with≡ y rewrite y = refl
-  canonicalIdempotent (zero :: a) | (x :: bl) with≡ y = transitivity (equalityCommutative (canonicalAscends' {zero} a λ p → contr p y)) (transitivity (applyEquality (zero ::_) (canonicalIdempotent a)) (equalityCommutative v))
-    where
-      contr : {a : _} {A : Set a} {l1 l2 : List A} → {x : A} → l1 ≡ [] → l1 ≡ x :: l2 → False
-      contr {l1 = []} p1 ()
-      contr {l1 = x :: l1} () p2
-      u : canonical (canonical (zero :: a)) ≡ canonical (zero :: canonical a)
-      u = applyEquality canonical (equalityCommutative (canonicalAscends' {zero} a λ p → contr p y))
-      v : canonical (canonical (zero :: a)) ≡ zero :: canonical (canonical a)
-      v = transitivity u (equalityCommutative (canonicalAscends' {zero} (canonical a) λ p → contr (transitivity (canonicalIdempotent a) p) y))
-  canonicalIdempotent (one :: a) rewrite equalityCommutative (canonicalIdempotent a) = refl
+canonicalIdempotent : (a : BinNat) → canonical a ≡ canonical (canonical a)
+canonicalIdempotent [] = refl
+canonicalIdempotent (zero :: a) with inspect (canonical a)
+canonicalIdempotent (zero :: a) | [] with≡ y rewrite y = refl
+canonicalIdempotent (zero :: a) | (x :: bl) with≡ y = transitivity (equalityCommutative (canonicalAscends' {zero} a λ p → contr p y)) (transitivity (applyEquality (zero ::_) (canonicalIdempotent a)) (equalityCommutative v))
+  where
+    contr : {a : _} {A : Set a} {l1 l2 : List A} → {x : A} → l1 ≡ [] → l1 ≡ x :: l2 → False
+    contr {l1 = []} p1 ()
+    contr {l1 = x :: l1} () p2
+    u : canonical (canonical (zero :: a)) ≡ canonical (zero :: canonical a)
+    u = applyEquality canonical (equalityCommutative (canonicalAscends' {zero} a λ p → contr p y))
+    v : canonical (canonical (zero :: a)) ≡ zero :: canonical (canonical a)
+    v = transitivity u (equalityCommutative (canonicalAscends' {zero} (canonical a) λ p → contr (transitivity (canonicalIdempotent a) p) y))
+canonicalIdempotent (one :: a) rewrite equalityCommutative (canonicalIdempotent a) = refl
 
-  canonicalAscends'' : {i : Bit} → (a : BinNat) → canonical (i :: canonical a) ≡ canonical (i :: a)
+canonicalAscends'' : {i : Bit} → (a : BinNat) → canonical (i :: canonical a) ≡ canonical (i :: a)
 
-  binNatToNInj : (x y : BinNat) → binNatToN x ≡ binNatToN y → canonical x ≡ canonical y
+binNatToNInj : (x y : BinNat) → binNatToN x ≡ binNatToN y → canonical x ≡ canonical y
 
-  NToBinNatInj : (x y : ℕ) → canonical (NToBinNat x) ≡ canonical (NToBinNat y) → x ≡ y
+NToBinNatInj : (x y : ℕ) → canonical (NToBinNat x) ≡ canonical (NToBinNat y) → x ≡ y
 
-  NToBinNatIsCanonical : (x : ℕ) → NToBinNat x ≡ canonical (NToBinNat x)
-  NToBinNatIsCanonical zero = refl
-  NToBinNatIsCanonical (succ x) with NToBinNatC x
-  NToBinNatIsCanonical (succ x) | a , b = equalityCommutative (incrPreservesCanonical (NToBinNat x) (equalityCommutative (NToBinNatIsCanonical x)))
+NToBinNatIsCanonical : (x : ℕ) → NToBinNat x ≡ canonical (NToBinNat x)
+NToBinNatIsCanonical zero = refl
+NToBinNatIsCanonical (succ x) with NToBinNatC x
+NToBinNatIsCanonical (succ x) | a , b = equalityCommutative (incrPreservesCanonical (NToBinNat x) (equalityCommutative (NToBinNatIsCanonical x)))
 
-  contr' : {a : _} {A : Set a} {l1 l2 : List A} → {x : A} → l1 ≡ [] → l1 ≡ x :: l2 → False
-  contr' {l1 = []} p1 ()
-  contr' {l1 = x :: l1} () p2
+contr' : {a : _} {A : Set a} {l1 l2 : List A} → {x : A} → l1 ≡ [] → l1 ≡ x :: l2 → False
+contr' {l1 = []} p1 ()
+contr' {l1 = x :: l1} () p2
 
-  binNatToNIsCanonical : (x : BinNat) → binNatToN (canonical x) ≡ binNatToN x
-  binNatToNIsCanonical [] = refl
-  binNatToNIsCanonical (zero :: x) with inspect (canonical x)
-  binNatToNIsCanonical (zero :: x) | [] with≡ t rewrite t | binNatToNZero' x t = refl
-  binNatToNIsCanonical (zero :: x) | (x₁ :: bl) with≡ t rewrite (equalityCommutative (canonicalAscends' {zero} x λ p → contr' p t)) | binNatToNIsCanonical x = refl
-  binNatToNIsCanonical (one :: x) rewrite binNatToNIsCanonical x = refl
+binNatToNIsCanonical : (x : BinNat) → binNatToN (canonical x) ≡ binNatToN x
+binNatToNIsCanonical [] = refl
+binNatToNIsCanonical (zero :: x) with inspect (canonical x)
+binNatToNIsCanonical (zero :: x) | [] with≡ t rewrite t | binNatToNZero' x t = refl
+binNatToNIsCanonical (zero :: x) | (x₁ :: bl) with≡ t rewrite (equalityCommutative (canonicalAscends' {zero} x λ p → contr' p t)) | binNatToNIsCanonical x = refl
+binNatToNIsCanonical (one :: x) rewrite binNatToNIsCanonical x = refl
 
 -- The following two theorems demonstrate that Canonicalised is isomorphic to ℕ
 
-  nToN : (x : ℕ) → binNatToN (NToBinNat x) ≡ x
+nToN : (x : ℕ) → binNatToN (NToBinNat x) ≡ x
 
-  binToBin : (x : BinNat) → NToBinNat (binNatToN x) ≡ canonical x
-  binToBin x = transitivity (NToBinNatIsCanonical (binNatToN x)) (binNatToNInj (NToBinNat (binNatToN x)) x (nToN (binNatToN x)))
+binToBin : (x : BinNat) → NToBinNat (binNatToN x) ≡ canonical x
+binToBin x = transitivity (NToBinNatIsCanonical (binNatToN x)) (binNatToNInj (NToBinNat (binNatToN x)) x (nToN (binNatToN x)))
 
-  doubleIsBitShift' : (a : ℕ) → NToBinNat (2 *N succ a) ≡ zero :: NToBinNat (succ a)
-  doubleIsBitShift' zero = refl
-  doubleIsBitShift' (succ a) with doubleIsBitShift' a
-  ... | bl rewrite Semiring.commutative ℕSemiring a (succ (succ (a +N 0))) | Semiring.commutative ℕSemiring (succ (a +N 0)) a | Semiring.commutative ℕSemiring a (succ (a +N 0)) | Semiring.commutative ℕSemiring (a +N 0) a | bl = refl
+doubleIsBitShift' : (a : ℕ) → NToBinNat (2 *N succ a) ≡ zero :: NToBinNat (succ a)
+doubleIsBitShift' zero = refl
+doubleIsBitShift' (succ a) with doubleIsBitShift' a
+... | bl rewrite Semiring.commutative ℕSemiring a (succ (succ (a +N 0))) | Semiring.commutative ℕSemiring (succ (a +N 0)) a | Semiring.commutative ℕSemiring a (succ (a +N 0)) | Semiring.commutative ℕSemiring (a +N 0) a | bl = refl
 
-  doubleIsBitShift : (a : ℕ) → (0 <N a) → NToBinNat (2 *N a) ≡ zero :: NToBinNat a
-  doubleIsBitShift zero ()
-  doubleIsBitShift (succ a) _ = doubleIsBitShift' a
+doubleIsBitShift : (a : ℕ) → (0 <N a) → NToBinNat (2 *N a) ≡ zero :: NToBinNat a
+doubleIsBitShift zero ()
+doubleIsBitShift (succ a) _ = doubleIsBitShift' a
 
-  canonicalDescends : {a : Bit} (as : BinNat) → (prA : a :: as ≡ canonical (a :: as)) → as ≡ canonical as
-  canonicalDescends {zero} as pr with canonical as
-  canonicalDescends {zero} as pr | x :: bl = ::Inj pr
-  canonicalDescends {one} as pr = ::Inj pr
+canonicalDescends : {a : Bit} (as : BinNat) → (prA : a :: as ≡ canonical (a :: as)) → as ≡ canonical as
+canonicalDescends {zero} as pr with canonical as
+canonicalDescends {zero} as pr | x :: bl = ::Inj pr
+canonicalDescends {one} as pr = ::Inj pr
 
 --- Proofs
 
-  parity : (a b : ℕ) → succ (2 *N a) ≡ 2 *N b → False
-  doubleInj : (a b : ℕ) → (2 *N a) ≡ (2 *N b) → a ≡ b
+parity : (a b : ℕ) → succ (2 *N a) ≡ 2 *N b → False
+doubleInj : (a b : ℕ) → (2 *N a) ≡ (2 *N b) → a ≡ b
 
-  incrNonzeroTwice : (x : BinNat) → canonical (incr (incr x)) ≡ one :: [] → False
-  incrNonzeroTwice (zero :: xs) pr with canonical (incr xs)
-  incrNonzeroTwice (zero :: xs) () | []
-  incrNonzeroTwice (zero :: xs) () | x :: bl
-  incrNonzeroTwice (one :: xs) pr = exFalso (incrNonzero xs (::Inj pr))
+incrNonzeroTwice : (x : BinNat) → canonical (incr (incr x)) ≡ one :: [] → False
+incrNonzeroTwice (zero :: xs) pr with canonical (incr xs)
+incrNonzeroTwice (zero :: xs) () | []
+incrNonzeroTwice (zero :: xs) () | x :: bl
+incrNonzeroTwice (one :: xs) pr = exFalso (incrNonzero xs (::Inj pr))
 
-  canonicalRespectsIncr' {[]} {[]} pr = refl
-  canonicalRespectsIncr' {[]} {zero :: y} pr with canonical y
-  canonicalRespectsIncr' {[]} {zero :: y} pr | [] = refl
-  canonicalRespectsIncr' {[]} {one :: y} pr with canonical (incr y)
-  canonicalRespectsIncr' {[]} {one :: y} () | []
-  canonicalRespectsIncr' {[]} {one :: y} () | x :: bl
-  canonicalRespectsIncr' {zero :: xs} {y} pr with canonical xs
-  canonicalRespectsIncr' {zero :: xs} {[]} pr | [] = refl
-  canonicalRespectsIncr' {zero :: xs} {zero :: y} pr | [] with canonical y
-  canonicalRespectsIncr' {zero :: xs} {zero :: y} pr | [] | [] = refl
-  canonicalRespectsIncr' {zero :: xs} {one :: y} pr | [] with canonical (incr y)
-  canonicalRespectsIncr' {zero :: xs} {one :: y} () | [] | []
-  canonicalRespectsIncr' {zero :: xs} {one :: y} () | [] | x :: bl
-  canonicalRespectsIncr' {zero :: xs} {zero :: ys} pr | x :: bl with canonical ys
-  canonicalRespectsIncr' {zero :: xs} {zero :: ys} pr | x :: bl | x₁ :: th = applyEquality (zero ::_) (::Inj pr)
-  canonicalRespectsIncr' {zero :: xs} {one :: ys} pr | x :: bl with canonical (incr ys)
-  canonicalRespectsIncr' {zero :: xs} {one :: ys} () | x :: bl | []
-  canonicalRespectsIncr' {zero :: xs} {one :: ys} () | x :: bl | x₁ :: th
-  canonicalRespectsIncr' {one :: xs} {[]} pr with canonical (incr xs)
-  canonicalRespectsIncr' {one :: xs} {[]} () | []
-  canonicalRespectsIncr' {one :: xs} {[]} () | x :: bl
-  canonicalRespectsIncr' {one :: xs} {zero :: ys} pr with canonical ys
-  canonicalRespectsIncr' {one :: xs} {zero :: ys} pr | [] with canonical (incr xs)
-  canonicalRespectsIncr' {one :: xs} {zero :: ys} () | [] | []
-  canonicalRespectsIncr' {one :: xs} {zero :: ys} () | [] | x :: t
-  canonicalRespectsIncr' {one :: xs} {zero :: ys} pr | x :: bl with canonical (incr xs)
-  canonicalRespectsIncr' {one :: xs} {zero :: ys} () | x :: bl | []
-  canonicalRespectsIncr' {one :: xs} {zero :: ys} () | x :: bl | x₁ :: t
-  canonicalRespectsIncr' {one :: xs} {one :: ys} pr with inspect (canonical (incr xs))
-  canonicalRespectsIncr' {one :: xs} {one :: ys} pr | [] with≡ x = exFalso (incrNonzero xs x)
-  canonicalRespectsIncr' {one :: xs} {one :: ys} pr | (x+1 :: x+1s) with≡ bad rewrite bad = applyEquality (one ::_) ans
-    where
-      ans : canonical xs ≡ canonical ys
-      ans with inspect (canonical (incr ys))
-      ans | [] with≡ x = exFalso (incrNonzero ys x)
-      ans | (x₁ :: y) with≡ x rewrite x = canonicalRespectsIncr' {xs} {ys} (transitivity bad (transitivity (::Inj pr) (equalityCommutative x)))
+canonicalRespectsIncr' {[]} {[]} pr = refl
+canonicalRespectsIncr' {[]} {zero :: y} pr with canonical y
+canonicalRespectsIncr' {[]} {zero :: y} pr | [] = refl
+canonicalRespectsIncr' {[]} {one :: y} pr with canonical (incr y)
+canonicalRespectsIncr' {[]} {one :: y} () | []
+canonicalRespectsIncr' {[]} {one :: y} () | x :: bl
+canonicalRespectsIncr' {zero :: xs} {y} pr with canonical xs
+canonicalRespectsIncr' {zero :: xs} {[]} pr | [] = refl
+canonicalRespectsIncr' {zero :: xs} {zero :: y} pr | [] with canonical y
+canonicalRespectsIncr' {zero :: xs} {zero :: y} pr | [] | [] = refl
+canonicalRespectsIncr' {zero :: xs} {one :: y} pr | [] with canonical (incr y)
+canonicalRespectsIncr' {zero :: xs} {one :: y} () | [] | []
+canonicalRespectsIncr' {zero :: xs} {one :: y} () | [] | x :: bl
+canonicalRespectsIncr' {zero :: xs} {zero :: ys} pr | x :: bl with canonical ys
+canonicalRespectsIncr' {zero :: xs} {zero :: ys} pr | x :: bl | x₁ :: th = applyEquality (zero ::_) (::Inj pr)
+canonicalRespectsIncr' {zero :: xs} {one :: ys} pr | x :: bl with canonical (incr ys)
+canonicalRespectsIncr' {zero :: xs} {one :: ys} () | x :: bl | []
+canonicalRespectsIncr' {zero :: xs} {one :: ys} () | x :: bl | x₁ :: th
+canonicalRespectsIncr' {one :: xs} {[]} pr with canonical (incr xs)
+canonicalRespectsIncr' {one :: xs} {[]} () | []
+canonicalRespectsIncr' {one :: xs} {[]} () | x :: bl
+canonicalRespectsIncr' {one :: xs} {zero :: ys} pr with canonical ys
+canonicalRespectsIncr' {one :: xs} {zero :: ys} pr | [] with canonical (incr xs)
+canonicalRespectsIncr' {one :: xs} {zero :: ys} () | [] | []
+canonicalRespectsIncr' {one :: xs} {zero :: ys} () | [] | x :: t
+canonicalRespectsIncr' {one :: xs} {zero :: ys} pr | x :: bl with canonical (incr xs)
+canonicalRespectsIncr' {one :: xs} {zero :: ys} () | x :: bl | []
+canonicalRespectsIncr' {one :: xs} {zero :: ys} () | x :: bl | x₁ :: t
+canonicalRespectsIncr' {one :: xs} {one :: ys} pr with inspect (canonical (incr xs))
+canonicalRespectsIncr' {one :: xs} {one :: ys} pr | [] with≡ x = exFalso (incrNonzero xs x)
+canonicalRespectsIncr' {one :: xs} {one :: ys} pr | (x+1 :: x+1s) with≡ bad rewrite bad = applyEquality (one ::_) ans
+  where
+    ans : canonical xs ≡ canonical ys
+    ans with inspect (canonical (incr ys))
+    ans | [] with≡ x = exFalso (incrNonzero ys x)
+    ans | (x₁ :: y) with≡ x rewrite x = canonicalRespectsIncr' {xs} {ys} (transitivity bad (transitivity (::Inj pr) (equalityCommutative x)))
 
-  binNatToNInj[] : (y : BinNat) → 0 ≡ binNatToN y → [] ≡ canonical y
-  binNatToNInj[] [] pr = refl
-  binNatToNInj[] (zero :: y) pr with productZeroImpliesOperandZero {2} {binNatToN y} (equalityCommutative pr)
-  binNatToNInj[] (zero :: y) pr | inr x with inspect (canonical y)
-  binNatToNInj[] (zero :: y) pr | inr x | [] with≡ canYPr rewrite canYPr = refl
-  binNatToNInj[] (zero :: ys) pr | inr x | (y :: canY) with≡ canYPr with binNatToNZero ys x
-  ... | r with canonical ys
-  binNatToNInj[] (zero :: ys) pr | inr x | (y :: canY) with≡ canYPr | r | [] = refl
-  binNatToNInj[] (zero :: ys) pr | inr x | (y :: canY) with≡ canYPr | () | x₁ :: t
+binNatToNInj[] : (y : BinNat) → 0 ≡ binNatToN y → [] ≡ canonical y
+binNatToNInj[] [] pr = refl
+binNatToNInj[] (zero :: y) pr with productZeroImpliesOperandZero {2} {binNatToN y} (equalityCommutative pr)
+binNatToNInj[] (zero :: y) pr | inr x with inspect (canonical y)
+binNatToNInj[] (zero :: y) pr | inr x | [] with≡ canYPr rewrite canYPr = refl
+binNatToNInj[] (zero :: ys) pr | inr x | (y :: canY) with≡ canYPr with binNatToNZero ys x
+... | r with canonical ys
+binNatToNInj[] (zero :: ys) pr | inr x | (y :: canY) with≡ canYPr | r | [] = refl
+binNatToNInj[] (zero :: ys) pr | inr x | (y :: canY) with≡ canYPr | () | x₁ :: t
 
-  binNatToNInj [] y pr = binNatToNInj[] y pr
-  binNatToNInj (zero :: xs) [] pr = equalityCommutative (binNatToNInj[] (zero :: xs) (equalityCommutative pr))
-  binNatToNInj (zero :: xs) (zero :: ys) pr with doubleInj (binNatToN xs) (binNatToN ys) pr
-  ... | x=y with binNatToNInj xs ys x=y
-  ... | t with canonical xs
-  binNatToNInj (zero :: xs) (zero :: ys) pr | x=y | t | [] with canonical ys
-  binNatToNInj (zero :: xs) (zero :: ys) pr | x=y | t | [] | [] = refl
-  binNatToNInj (zero :: xs) (zero :: ys) pr | x=y | t | x :: cxs with canonical ys
-  binNatToNInj (zero :: xs) (zero :: ys) pr | x=y | t | x :: cxs | x₁ :: cys = applyEquality (zero ::_) t
-  binNatToNInj (zero :: xs) (one :: ys) pr = exFalso (parity (binNatToN ys) (binNatToN xs) (equalityCommutative pr))
-  binNatToNInj (one :: xs) (zero :: ys) pr = exFalso (parity (binNatToN xs) (binNatToN ys) pr)
-  binNatToNInj (one :: xs) (one :: ys) pr = applyEquality (one ::_) (binNatToNInj xs ys (doubleInj (binNatToN xs) (binNatToN ys) (succInjective pr)))
+binNatToNInj [] y pr = binNatToNInj[] y pr
+binNatToNInj (zero :: xs) [] pr = equalityCommutative (binNatToNInj[] (zero :: xs) (equalityCommutative pr))
+binNatToNInj (zero :: xs) (zero :: ys) pr with doubleInj (binNatToN xs) (binNatToN ys) pr
+... | x=y with binNatToNInj xs ys x=y
+... | t with canonical xs
+binNatToNInj (zero :: xs) (zero :: ys) pr | x=y | t | [] with canonical ys
+binNatToNInj (zero :: xs) (zero :: ys) pr | x=y | t | [] | [] = refl
+binNatToNInj (zero :: xs) (zero :: ys) pr | x=y | t | x :: cxs with canonical ys
+binNatToNInj (zero :: xs) (zero :: ys) pr | x=y | t | x :: cxs | x₁ :: cys = applyEquality (zero ::_) t
+binNatToNInj (zero :: xs) (one :: ys) pr = exFalso (parity (binNatToN ys) (binNatToN xs) (equalityCommutative pr))
+binNatToNInj (one :: xs) (zero :: ys) pr = exFalso (parity (binNatToN xs) (binNatToN ys) pr)
+binNatToNInj (one :: xs) (one :: ys) pr = applyEquality (one ::_) (binNatToNInj xs ys (doubleInj (binNatToN xs) (binNatToN ys) (succInjective pr)))
 
-  NToBinNatInj zero zero pr = refl
-  NToBinNatInj zero (succ y) pr with NToBinNat y
-  NToBinNatInj zero (succ y) pr | bl = exFalso (incrNonzero bl (equalityCommutative pr))
-  NToBinNatInj (succ x) zero pr with NToBinNat x
-  ... | bl = exFalso (incrNonzero bl pr)
-  NToBinNatInj (succ x) (succ y) pr with inspect (NToBinNat x)
-  NToBinNatInj (succ zero) (succ zero) pr | [] with≡ nToBinXPr = refl
-  NToBinNatInj (succ zero) (succ (succ y)) pr | [] with≡ nToBinXPr with NToBinNat y
-  NToBinNatInj (succ zero) (succ (succ y)) pr | [] with≡ nToBinXPr | y' = exFalso (incrNonzeroTwice y' (equalityCommutative pr))
-  NToBinNatInj (succ (succ x)) (succ y) pr | [] with≡ nToBinXPr with NToBinNat x
-  NToBinNatInj (succ (succ x)) (succ y) pr | [] with≡ nToBinXPr | t = exFalso (incrNonzero' t nToBinXPr)
-  NToBinNatInj (succ x) (succ y) pr | (x₁ :: nToBinX) with≡ nToBinXPr with NToBinNatInj x y (canonicalRespectsIncr' {NToBinNat x} {NToBinNat y} pr)
-  NToBinNatInj (succ x) (succ .x) pr | (x₁ :: nToBinX) with≡ nToBinXPr | refl = refl
+NToBinNatInj zero zero pr = refl
+NToBinNatInj zero (succ y) pr with NToBinNat y
+NToBinNatInj zero (succ y) pr | bl = exFalso (incrNonzero bl (equalityCommutative pr))
+NToBinNatInj (succ x) zero pr with NToBinNat x
+... | bl = exFalso (incrNonzero bl pr)
+NToBinNatInj (succ x) (succ y) pr with inspect (NToBinNat x)
+NToBinNatInj (succ zero) (succ zero) pr | [] with≡ nToBinXPr = refl
+NToBinNatInj (succ zero) (succ (succ y)) pr | [] with≡ nToBinXPr with NToBinNat y
+NToBinNatInj (succ zero) (succ (succ y)) pr | [] with≡ nToBinXPr | y' = exFalso (incrNonzeroTwice y' (equalityCommutative pr))
+NToBinNatInj (succ (succ x)) (succ y) pr | [] with≡ nToBinXPr with NToBinNat x
+NToBinNatInj (succ (succ x)) (succ y) pr | [] with≡ nToBinXPr | t = exFalso (incrNonzero' t nToBinXPr)
+NToBinNatInj (succ x) (succ y) pr | (x₁ :: nToBinX) with≡ nToBinXPr with NToBinNatInj x y (canonicalRespectsIncr' {NToBinNat x} {NToBinNat y} pr)
+NToBinNatInj (succ x) (succ .x) pr | (x₁ :: nToBinX) with≡ nToBinXPr | refl = refl
 
-  incrInj {[]} {[]} pr = refl
-  incrInj {[]} {zero :: ys} pr rewrite equalityCommutative (::Inj pr) = refl
-  incrInj {zero :: xs} {[]} pr rewrite ::Inj pr = refl
-  incrInj {zero :: xs} {zero :: .xs} refl = refl
-  incrInj {one :: xs} {one :: ys} pr = applyEquality (one ::_) (incrInj {xs} {ys} (l (incr xs) (incr ys) pr))
-    where
-      l : (a : BinNat) → (b : BinNat) → zero :: a ≡ zero :: b → a ≡ b
-      l a .a refl = refl
+incrInj {[]} {[]} pr = refl
+incrInj {[]} {zero :: ys} pr rewrite equalityCommutative (::Inj pr) = refl
+incrInj {zero :: xs} {[]} pr rewrite ::Inj pr = refl
+incrInj {zero :: xs} {zero :: .xs} refl = refl
+incrInj {one :: xs} {one :: ys} pr = applyEquality (one ::_) (incrInj {xs} {ys} (l (incr xs) (incr ys) pr))
+  where
+    l : (a : BinNat) → (b : BinNat) → zero :: a ≡ zero :: b → a ≡ b
+    l a .a refl = refl
 
-  doubleInj zero zero pr = refl
-  doubleInj (succ a) (succ b) pr = applyEquality succ (doubleInj a b u)
-    where
-      t : a +N a ≡ b +N b
-      t rewrite Semiring.commutative ℕSemiring (succ a) 0 | Semiring.commutative ℕSemiring (succ b) 0 | Semiring.commutative ℕSemiring a (succ a) | Semiring.commutative ℕSemiring b (succ b) = succInjective (succInjective pr)
-      u : a +N (a +N zero) ≡ b +N (b +N zero)
-      u rewrite Semiring.commutative ℕSemiring a 0 | Semiring.commutative ℕSemiring b 0 = t
+doubleInj zero zero pr = refl
+doubleInj (succ a) (succ b) pr = applyEquality succ (doubleInj a b u)
+  where
+    t : a +N a ≡ b +N b
+    t rewrite Semiring.commutative ℕSemiring (succ a) 0 | Semiring.commutative ℕSemiring (succ b) 0 | Semiring.commutative ℕSemiring a (succ a) | Semiring.commutative ℕSemiring b (succ b) = succInjective (succInjective pr)
+    u : a +N (a +N zero) ≡ b +N (b +N zero)
+    u rewrite Semiring.commutative ℕSemiring a 0 | Semiring.commutative ℕSemiring b 0 = t
 
-  binNatToNZero [] pr = refl
-  binNatToNZero (zero :: xs) pr with inspect (canonical xs)
-  binNatToNZero (zero :: xs) pr | [] with≡ x rewrite x = refl
-  binNatToNZero (zero :: xs) pr | (x₁ :: y) with≡ x with productZeroImpliesOperandZero {2} {binNatToN xs} pr
-  binNatToNZero (zero :: xs) pr | (x₁ :: y) with≡ x | inr pr' with binNatToNZero xs pr'
-  ... | bl with canonical xs
-  binNatToNZero (zero :: xs) pr | (x₁ :: y) with≡ x | inr pr' | bl | [] = refl
-  binNatToNZero (zero :: xs) pr | (x₁ :: y) with≡ x | inr pr' | () | x₂ :: t
+binNatToNZero [] pr = refl
+binNatToNZero (zero :: xs) pr with inspect (canonical xs)
+binNatToNZero (zero :: xs) pr | [] with≡ x rewrite x = refl
+binNatToNZero (zero :: xs) pr | (x₁ :: y) with≡ x with productZeroImpliesOperandZero {2} {binNatToN xs} pr
+binNatToNZero (zero :: xs) pr | (x₁ :: y) with≡ x | inr pr' with binNatToNZero xs pr'
+... | bl with canonical xs
+binNatToNZero (zero :: xs) pr | (x₁ :: y) with≡ x | inr pr' | bl | [] = refl
+binNatToNZero (zero :: xs) pr | (x₁ :: y) with≡ x | inr pr' | () | x₂ :: t
 
-  binNatToNSucc [] = refl
-  binNatToNSucc (zero :: n) = refl
-  binNatToNSucc (one :: n) rewrite Semiring.commutative ℕSemiring (binNatToN n) zero | Semiring.commutative ℕSemiring (binNatToN (incr n)) 0 | binNatToNSucc n = applyEquality succ (Semiring.commutative ℕSemiring (binNatToN n) (succ (binNatToN n)))
+binNatToNSucc [] = refl
+binNatToNSucc (zero :: n) = refl
+binNatToNSucc (one :: n) rewrite Semiring.commutative ℕSemiring (binNatToN n) zero | Semiring.commutative ℕSemiring (binNatToN (incr n)) 0 | binNatToNSucc n = applyEquality succ (Semiring.commutative ℕSemiring (binNatToN n) (succ (binNatToN n)))
 
-  incrNonzero (one :: xs) pr with inspect (canonical (incr xs))
-  incrNonzero (one :: xs) pr | [] with≡ x = incrNonzero xs x
-  incrNonzero (one :: xs) pr | (y :: ys) with≡ x with canonical (incr xs)
-  incrNonzero (one :: xs) pr | (y :: ys) with≡ () | []
-  incrNonzero (one :: xs) () | (.x₁ :: .th) with≡ refl | x₁ :: th
+incrNonzero (one :: xs) pr with inspect (canonical (incr xs))
+incrNonzero (one :: xs) pr | [] with≡ x = incrNonzero xs x
+incrNonzero (one :: xs) pr | (y :: ys) with≡ x with canonical (incr xs)
+incrNonzero (one :: xs) pr | (y :: ys) with≡ () | []
+incrNonzero (one :: xs) () | (.x₁ :: .th) with≡ refl | x₁ :: th
 
-  nToN zero = refl
-  nToN (succ x) with inspect (NToBinNat x)
-  nToN (succ x) | [] with≡ pr = ans
-    where
-      t : x ≡ zero
-      t = NToBinNatInj x 0 (applyEquality canonical pr)
-      ans : binNatToN (incr (NToBinNat x)) ≡ succ x
-      ans rewrite t | pr = refl
-  nToN (succ x) | (bit :: xs) with≡ pr = transitivity (binNatToNSucc (NToBinNat x)) (applyEquality succ (nToN x))
+nToN zero = refl
+nToN (succ x) with inspect (NToBinNat x)
+nToN (succ x) | [] with≡ pr = ans
+  where
+    t : x ≡ zero
+    t = NToBinNatInj x 0 (applyEquality canonical pr)
+    ans : binNatToN (incr (NToBinNat x)) ≡ succ x
+    ans rewrite t | pr = refl
+nToN (succ x) | (bit :: xs) with≡ pr = transitivity (binNatToNSucc (NToBinNat x)) (applyEquality succ (nToN x))
 
-  parity zero (succ b) pr rewrite Semiring.commutative ℕSemiring b (succ (b +N 0)) = bad pr
-    where
-      bad : (1 ≡ succ (succ ((b +N 0) +N b))) → False
-      bad ()
-  parity (succ a) (succ b) pr rewrite Semiring.commutative ℕSemiring b (succ (b +N 0)) | Semiring.commutative ℕSemiring a (succ (a +N 0)) | Semiring.commutative ℕSemiring (a +N 0) a | Semiring.commutative ℕSemiring (b +N 0) b = parity a b (succInjective (succInjective pr))
+parity zero (succ b) pr rewrite Semiring.commutative ℕSemiring b (succ (b +N 0)) = bad pr
+  where
+    bad : (1 ≡ succ (succ ((b +N 0) +N b))) → False
+    bad ()
+parity (succ a) (succ b) pr rewrite Semiring.commutative ℕSemiring b (succ (b +N 0)) | Semiring.commutative ℕSemiring a (succ (a +N 0)) | Semiring.commutative ℕSemiring (a +N 0) a | Semiring.commutative ℕSemiring (b +N 0) b = parity a b (succInjective (succInjective pr))
 
-  binNatToNZero' [] pr = refl
-  binNatToNZero' (zero :: xs) pr with inspect (canonical xs)
-  binNatToNZero' (zero :: xs) pr | [] with≡ p2 = ans
-    where
-      t : binNatToN xs ≡ 0
-      t = binNatToNZero' xs p2
-      ans : 2 *N binNatToN xs ≡ 0
-      ans rewrite t = refl
-  binNatToNZero' (zero :: xs) pr | (y :: ys) with≡ p rewrite p = exFalso (bad pr)
-    where
-      bad : zero :: y :: ys ≡ [] → False
-      bad ()
-  binNatToNZero' (one :: xs) ()
+binNatToNZero' [] pr = refl
+binNatToNZero' (zero :: xs) pr with inspect (canonical xs)
+binNatToNZero' (zero :: xs) pr | [] with≡ p2 = ans
+  where
+    t : binNatToN xs ≡ 0
+    t = binNatToNZero' xs p2
+    ans : 2 *N binNatToN xs ≡ 0
+    ans rewrite t = refl
+binNatToNZero' (zero :: xs) pr | (y :: ys) with≡ p rewrite p = exFalso (bad pr)
+  where
+    bad : zero :: y :: ys ≡ [] → False
+    bad ()
+binNatToNZero' (one :: xs) ()
 
-  canonicalAscends {zero} a 0<a with inspect (canonical a)
-  canonicalAscends {zero} (zero :: a) 0<a | [] with≡ x = exFalso (contr'' (binNatToN a) t v)
-    where
-      u : binNatToN (zero :: a) ≡ 0
-      u = binNatToNZero' (zero :: a) x
-      v : binNatToN a ≡ 0
-      v with inspect (binNatToN a)
-      v | zero with≡ x = x
-      v | succ a' with≡ x with inspect (binNatToN (zero :: a))
-      v | succ a' with≡ x | zero with≡ pr2 rewrite pr2 = exFalso (TotalOrder.irreflexive ℕTotalOrder 0<a)
-      v | succ a' with≡ x | succ y with≡ pr2 rewrite u = exFalso (TotalOrder.irreflexive ℕTotalOrder 0<a)
-      t : 0 <N binNatToN a
-      t with binNatToN a
-      t | succ bl rewrite Semiring.commutative ℕSemiring (succ bl) 0 = succIsPositive bl
-      contr'' : (x : ℕ) → (0 <N x) → (x ≡ 0) → False
-      contr'' x 0<x x=0 rewrite x=0 = TotalOrder.irreflexive ℕTotalOrder 0<x
-  canonicalAscends {zero} a 0<a | (x₁ :: y) with≡ x rewrite x = refl
-  canonicalAscends {one} a 0<a = refl
+canonicalAscends {zero} a 0<a with inspect (canonical a)
+canonicalAscends {zero} (zero :: a) 0<a | [] with≡ x = exFalso (contr'' (binNatToN a) t v)
+  where
+    u : binNatToN (zero :: a) ≡ 0
+    u = binNatToNZero' (zero :: a) x
+    v : binNatToN a ≡ 0
+    v with inspect (binNatToN a)
+    v | zero with≡ x = x
+    v | succ a' with≡ x with inspect (binNatToN (zero :: a))
+    v | succ a' with≡ x | zero with≡ pr2 rewrite pr2 = exFalso (TotalOrder.irreflexive ℕTotalOrder 0<a)
+    v | succ a' with≡ x | succ y with≡ pr2 rewrite u = exFalso (TotalOrder.irreflexive ℕTotalOrder 0<a)
+    t : 0 <N binNatToN a
+    t with binNatToN a
+    t | succ bl rewrite Semiring.commutative ℕSemiring (succ bl) 0 = succIsPositive bl
+    contr'' : (x : ℕ) → (0 <N x) → (x ≡ 0) → False
+    contr'' x 0<x x=0 rewrite x=0 = TotalOrder.irreflexive ℕTotalOrder 0<x
+canonicalAscends {zero} a 0<a | (x₁ :: y) with≡ x rewrite x = refl
+canonicalAscends {one} a 0<a = refl
 
-  canonicalAscends'' {i} a with inspect (canonical a)
-  canonicalAscends'' {zero} a | [] with≡ x rewrite x = refl
-  canonicalAscends'' {one} a | [] with≡ x rewrite x = refl
-  canonicalAscends'' {i} a | (x₁ :: y) with≡ x = transitivity (applyEquality canonical (canonicalAscends' {i} a λ p → contr p x)) (equalityCommutative (canonicalIdempotent (i :: a)))
-    where
-      contr : {a : _} {A : Set a} {l1 l2 : List A} → {x : A} → l1 ≡ [] → l1 ≡ x :: l2 → False
-      contr {l1 = []} p1 ()
-      contr {l1 = x :: l1} () p2
+canonicalAscends'' {i} a with inspect (canonical a)
+canonicalAscends'' {zero} a | [] with≡ x rewrite x = refl
+canonicalAscends'' {one} a | [] with≡ x rewrite x = refl
+canonicalAscends'' {i} a | (x₁ :: y) with≡ x = transitivity (applyEquality canonical (canonicalAscends' {i} a λ p → contr p x)) (equalityCommutative (canonicalIdempotent (i :: a)))
+  where
+    contr : {a : _} {A : Set a} {l1 l2 : List A} → {x : A} → l1 ≡ [] → l1 ≡ x :: l2 → False
+    contr {l1 = []} p1 ()
+    contr {l1 = x :: l1} () p2
 
-  incrPreservesCanonical' [] = refl
-  incrPreservesCanonical' (zero :: xs) with inspect (canonical xs)
-  incrPreservesCanonical' (zero :: xs) | [] with≡ x rewrite x = refl
-  incrPreservesCanonical' (zero :: xs) | (x₁ :: y) with≡ x rewrite x = refl
-  incrPreservesCanonical' (one :: xs) with inspect (canonical (incr xs))
-  ... | [] with≡ pr = exFalso (incrNonzero xs pr)
-  ... | (_ :: _) with≡ pr rewrite pr = applyEquality (zero ::_) (transitivity (equalityCommutative pr) (incrPreservesCanonical' xs))
+incrPreservesCanonical' [] = refl
+incrPreservesCanonical' (zero :: xs) with inspect (canonical xs)
+incrPreservesCanonical' (zero :: xs) | [] with≡ x rewrite x = refl
+incrPreservesCanonical' (zero :: xs) | (x₁ :: y) with≡ x rewrite x = refl
+incrPreservesCanonical' (one :: xs) with inspect (canonical (incr xs))
+... | [] with≡ pr = exFalso (incrNonzero xs pr)
+... | (_ :: _) with≡ pr rewrite pr = applyEquality (zero ::_) (transitivity (equalityCommutative pr) (incrPreservesCanonical' xs))
 
-  NToBinNatSucc zero = refl
-  NToBinNatSucc (succ n) with NToBinNat n
-  ... | [] = refl
-  ... | a :: as = refl
+NToBinNatSucc zero = refl
+NToBinNatSucc (succ n) with NToBinNat n
+... | [] = refl
+... | a :: as = refl
diff --git a/Numbers/BinaryNaturals/Multiplication.agda b/Numbers/BinaryNaturals/Multiplication.agda
index 157920e..4e0cdb6 100644
--- a/Numbers/BinaryNaturals/Multiplication.agda
+++ b/Numbers/BinaryNaturals/Multiplication.agda
@@ -12,172 +12,172 @@ open import Semirings.Definition
 
 module Numbers.BinaryNaturals.Multiplication where
 
-  _*Binherit_ : BinNat → BinNat → BinNat
-  a *Binherit b = NToBinNat (binNatToN a *N binNatToN b)
+_*Binherit_ : BinNat → BinNat → BinNat
+a *Binherit b = NToBinNat (binNatToN a *N binNatToN b)
 
-  _*B_ : BinNat → BinNat → BinNat
-  [] *B b = []
-  (zero :: a) *B b = zero :: (a *B b)
-  (one :: a) *B b = (zero :: (a *B b)) +B b
+_*B_ : BinNat → BinNat → BinNat
+[] *B b = []
+(zero :: a) *B b = zero :: (a *B b)
+(one :: a) *B b = (zero :: (a *B b)) +B b
 
-  contr : {a : _} {A : Set a} {l1 l2 : List A} → {x : A} → l1 ≡ [] → l1 ≡ x :: l2 → False
-  contr {l1 = []} p1 ()
-  contr {l1 = x :: l1} () p2
+contr : {a : _} {A : Set a} {l1 l2 : List A} → {x : A} → l1 ≡ [] → l1 ≡ x :: l2 → False
+contr {l1 = []} p1 ()
+contr {l1 = x :: l1} () p2
 
-  *BEmpty : (a : BinNat) → canonical (a *B []) ≡ []
-  *BEmpty [] = refl
-  *BEmpty (zero :: a) rewrite *BEmpty a = refl
-  *BEmpty (one :: a) rewrite *BEmpty a = refl
+*BEmpty : (a : BinNat) → canonical (a *B []) ≡ []
+*BEmpty [] = refl
+*BEmpty (zero :: a) rewrite *BEmpty a = refl
+*BEmpty (one :: a) rewrite *BEmpty a = refl
 
-  canonicalDistributesPlus : (a b : BinNat) → canonical (a +B b) ≡ canonical a +B canonical b
-  canonicalDistributesPlus a b = transitivity ans (+BIsInherited (canonical a) (canonical b) (canonicalIdempotent a) (canonicalIdempotent b))
-    where
-      ans : canonical (a +B b) ≡ NToBinNat (binNatToN (canonical a) +N binNatToN (canonical b))
-      ans rewrite binNatToNIsCanonical a | binNatToNIsCanonical b = equalityCommutative (+BIsInherited' a b)
+canonicalDistributesPlus : (a b : BinNat) → canonical (a +B b) ≡ canonical a +B canonical b
+canonicalDistributesPlus a b = transitivity ans (+BIsInherited (canonical a) (canonical b) (canonicalIdempotent a) (canonicalIdempotent b))
+  where
+    ans : canonical (a +B b) ≡ NToBinNat (binNatToN (canonical a) +N binNatToN (canonical b))
+    ans rewrite binNatToNIsCanonical a | binNatToNIsCanonical b = equalityCommutative (+BIsInherited' a b)
 
-  incrPullsOut : (a b : BinNat) → incr (a +B b) ≡ (incr a) +B b
-  incrPullsOut [] [] = refl
-  incrPullsOut [] (zero :: b) = refl
-  incrPullsOut [] (one :: b) = refl
-  incrPullsOut (zero :: a) [] = refl
-  incrPullsOut (zero :: a) (zero :: b) = refl
-  incrPullsOut (zero :: a) (one :: b) = refl
-  incrPullsOut (one :: a) [] = refl
-  incrPullsOut (one :: a) (zero :: b) = applyEquality (zero ::_) (incrPullsOut a b)
-  incrPullsOut (one :: a) (one :: b) = applyEquality (one ::_) (incrPullsOut a b)
+incrPullsOut : (a b : BinNat) → incr (a +B b) ≡ (incr a) +B b
+incrPullsOut [] [] = refl
+incrPullsOut [] (zero :: b) = refl
+incrPullsOut [] (one :: b) = refl
+incrPullsOut (zero :: a) [] = refl
+incrPullsOut (zero :: a) (zero :: b) = refl
+incrPullsOut (zero :: a) (one :: b) = refl
+incrPullsOut (one :: a) [] = refl
+incrPullsOut (one :: a) (zero :: b) = applyEquality (zero ::_) (incrPullsOut a b)
+incrPullsOut (one :: a) (one :: b) = applyEquality (one ::_) (incrPullsOut a b)
 
-  timesZero : (a b : BinNat) → canonical a ≡ [] → canonical (a *B b) ≡ []
-  timesZero [] b pr = refl
-  timesZero (zero :: a) b pr with inspect (canonical a)
-  timesZero (zero :: a) b pr | [] with≡ prA rewrite prA | timesZero a b prA = refl
-  timesZero (zero :: a) b pr | (a1 :: as) with≡ prA rewrite prA = exFalso (nonEmptyNotEmpty pr)
+timesZero : (a b : BinNat) → canonical a ≡ [] → canonical (a *B b) ≡ []
+timesZero [] b pr = refl
+timesZero (zero :: a) b pr with inspect (canonical a)
+timesZero (zero :: a) b pr | [] with≡ prA rewrite prA | timesZero a b prA = refl
+timesZero (zero :: a) b pr | (a1 :: as) with≡ prA rewrite prA = exFalso (nonEmptyNotEmpty pr)
 
-  timesZero'' : (a b : BinNat) → canonical (a *B b) ≡ [] → (canonical a ≡ []) || (canonical b ≡ [])
-  timesZero'' [] b pr = inl refl
-  timesZero'' (x :: a) [] pr = inr refl
-  timesZero'' (zero :: as) (zero :: bs) pr with inspect (canonical as)
-  timesZero'' (zero :: as) (zero :: bs) pr | y with≡ x with inspect (canonical bs)
-  timesZero'' (zero :: as) (zero :: bs) pr | [] with≡ prAs | y₁ with≡ prBs rewrite prAs = inl refl
-  timesZero'' (zero :: as) (zero :: bs) pr | (a1 :: a's) with≡ prAs | [] with≡ prBs rewrite prBs = inr refl
-  timesZero'' (zero :: as) (zero :: bs) pr | (a1 :: a's) with≡ prAs | (x :: y) with≡ prBs with inspect (canonical (as *B (zero :: bs)))
-  timesZero'' (zero :: as) (zero :: bs) pr | (a1 :: a's) with≡ prAs | (b1 :: b's) with≡ prBs | [] with≡ pr' with timesZero'' as (zero :: bs) pr'
-  timesZero'' (zero :: as) (zero :: bs) pr | (a1 :: a's) with≡ prAs | (b1 :: b's) with≡ prBs | [] with≡ pr' | inl x rewrite prAs | prBs | pr' | x = exFalso (nonEmptyNotEmpty x)
-  timesZero'' (zero :: as) (zero :: bs) pr | (a1 :: a's) with≡ prAs | (b1 :: b's) with≡ prBs | [] with≡ pr' | inr x rewrite prBs | pr' | x = exFalso (nonEmptyNotEmpty x)
-  timesZero'' (zero :: as) (zero :: bs) pr | (a1 :: a's) with≡ prAs | (b1 :: b's) with≡ prBs | (x :: y) with≡ pr' rewrite prAs | prBs | pr' = exFalso (nonEmptyNotEmpty pr)
-  timesZero'' (zero :: as) (one :: bs) pr with inspect (canonical as)
-  timesZero'' (zero :: as) (one :: bs) pr | [] with≡ x rewrite x = inl refl
-  timesZero'' (zero :: as) (one :: bs) pr | (a1 :: a's) with≡ x with inspect (canonical (as *B (one :: bs)))
-  timesZero'' (zero :: as) (one :: bs) pr | (a1 :: a's) with≡ x | [] with≡ pr' with timesZero'' as (one :: bs) pr'
-  timesZero'' (zero :: as) (one :: bs) pr | (a1 :: a's) with≡ x | [] with≡ pr' | inl pr'' rewrite x | pr' | pr'' = exFalso (nonEmptyNotEmpty pr'')
-  timesZero'' (zero :: as) (one :: bs) pr | (a1 :: a's) with≡ x | (x₁ :: y) with≡ pr' rewrite x | pr' = exFalso (nonEmptyNotEmpty pr)
-  timesZero'' (one :: as) (zero :: bs) pr with inspect (canonical bs)
-  timesZero'' (one :: as) (zero :: bs) pr | [] with≡ x rewrite x = inr refl
-  timesZero'' (one :: as) (zero :: bs) pr | (b1 :: b's) with≡ prB with inspect (canonical ((as *B (zero :: bs)) +B bs))
-  timesZero'' (one :: as) (zero :: bs) pr | (b1 :: b's) with≡ prB | [] with≡ x rewrite equalityCommutative (+BIsInherited' (as *B (zero :: bs)) bs) = exFalso (nonEmptyNotEmpty (transitivity (equalityCommutative prB) v))
-    where
-      t : binNatToN (as *B (zero :: bs)) +N binNatToN bs ≡ 0
-      t = transitivity (equalityCommutative (nToN _)) (applyEquality binNatToN x)
-      u : (binNatToN (as *B (zero :: bs)) ≡ 0) && (binNatToN bs ≡ 0)
-      u = sumZeroImpliesSummandsZero t
-      v : canonical bs ≡ []
-      v with u
-      ... | fst ,, snd = binNatToNZero bs snd
-  timesZero'' (one :: as) (zero :: bs) pr | (b1 :: b's) with≡ prB | (x₁ :: y) with≡ x rewrite prB | x = exFalso (nonEmptyNotEmpty pr)
+timesZero'' : (a b : BinNat) → canonical (a *B b) ≡ [] → (canonical a ≡ []) || (canonical b ≡ [])
+timesZero'' [] b pr = inl refl
+timesZero'' (x :: a) [] pr = inr refl
+timesZero'' (zero :: as) (zero :: bs) pr with inspect (canonical as)
+timesZero'' (zero :: as) (zero :: bs) pr | y with≡ x with inspect (canonical bs)
+timesZero'' (zero :: as) (zero :: bs) pr | [] with≡ prAs | y₁ with≡ prBs rewrite prAs = inl refl
+timesZero'' (zero :: as) (zero :: bs) pr | (a1 :: a's) with≡ prAs | [] with≡ prBs rewrite prBs = inr refl
+timesZero'' (zero :: as) (zero :: bs) pr | (a1 :: a's) with≡ prAs | (x :: y) with≡ prBs with inspect (canonical (as *B (zero :: bs)))
+timesZero'' (zero :: as) (zero :: bs) pr | (a1 :: a's) with≡ prAs | (b1 :: b's) with≡ prBs | [] with≡ pr' with timesZero'' as (zero :: bs) pr'
+timesZero'' (zero :: as) (zero :: bs) pr | (a1 :: a's) with≡ prAs | (b1 :: b's) with≡ prBs | [] with≡ pr' | inl x rewrite prAs | prBs | pr' | x = exFalso (nonEmptyNotEmpty x)
+timesZero'' (zero :: as) (zero :: bs) pr | (a1 :: a's) with≡ prAs | (b1 :: b's) with≡ prBs | [] with≡ pr' | inr x rewrite prBs | pr' | x = exFalso (nonEmptyNotEmpty x)
+timesZero'' (zero :: as) (zero :: bs) pr | (a1 :: a's) with≡ prAs | (b1 :: b's) with≡ prBs | (x :: y) with≡ pr' rewrite prAs | prBs | pr' = exFalso (nonEmptyNotEmpty pr)
+timesZero'' (zero :: as) (one :: bs) pr with inspect (canonical as)
+timesZero'' (zero :: as) (one :: bs) pr | [] with≡ x rewrite x = inl refl
+timesZero'' (zero :: as) (one :: bs) pr | (a1 :: a's) with≡ x with inspect (canonical (as *B (one :: bs)))
+timesZero'' (zero :: as) (one :: bs) pr | (a1 :: a's) with≡ x | [] with≡ pr' with timesZero'' as (one :: bs) pr'
+timesZero'' (zero :: as) (one :: bs) pr | (a1 :: a's) with≡ x | [] with≡ pr' | inl pr'' rewrite x | pr' | pr'' = exFalso (nonEmptyNotEmpty pr'')
+timesZero'' (zero :: as) (one :: bs) pr | (a1 :: a's) with≡ x | (x₁ :: y) with≡ pr' rewrite x | pr' = exFalso (nonEmptyNotEmpty pr)
+timesZero'' (one :: as) (zero :: bs) pr with inspect (canonical bs)
+timesZero'' (one :: as) (zero :: bs) pr | [] with≡ x rewrite x = inr refl
+timesZero'' (one :: as) (zero :: bs) pr | (b1 :: b's) with≡ prB with inspect (canonical ((as *B (zero :: bs)) +B bs))
+timesZero'' (one :: as) (zero :: bs) pr | (b1 :: b's) with≡ prB | [] with≡ x rewrite equalityCommutative (+BIsInherited' (as *B (zero :: bs)) bs) = exFalso (nonEmptyNotEmpty (transitivity (equalityCommutative prB) v))
+  where
+    t : binNatToN (as *B (zero :: bs)) +N binNatToN bs ≡ 0
+    t = transitivity (equalityCommutative (nToN _)) (applyEquality binNatToN x)
+    u : (binNatToN (as *B (zero :: bs)) ≡ 0) && (binNatToN bs ≡ 0)
+    u = sumZeroImpliesSummandsZero t
+    v : canonical bs ≡ []
+    v with u
+    ... | fst ,, snd = binNatToNZero bs snd
+timesZero'' (one :: as) (zero :: bs) pr | (b1 :: b's) with≡ prB | (x₁ :: y) with≡ x rewrite prB | x = exFalso (nonEmptyNotEmpty pr)
 
-  lemma : {i : Bit} → (a b : BinNat) → canonical a ≡ canonical b → canonical (i :: a) ≡ canonical (i :: b)
-  lemma {zero} a b pr with inspect (canonical a)
-  lemma {zero} a b pr | [] with≡ x rewrite x | equalityCommutative pr = refl
-  lemma {zero} a b pr | (a1 :: as) with≡ x rewrite x | equalityCommutative pr = refl
-  lemma {one} a b pr = applyEquality (one ::_) pr
+lemma : {i : Bit} → (a b : BinNat) → canonical a ≡ canonical b → canonical (i :: a) ≡ canonical (i :: b)
+lemma {zero} a b pr with inspect (canonical a)
+lemma {zero} a b pr | [] with≡ x rewrite x | equalityCommutative pr = refl
+lemma {zero} a b pr | (a1 :: as) with≡ x rewrite x | equalityCommutative pr = refl
+lemma {one} a b pr = applyEquality (one ::_) pr
 
-  binNatToNDistributesPlus : (a b : BinNat) → binNatToN (a +B b) ≡ binNatToN a +N binNatToN b
-  binNatToNDistributesPlus a b = transitivity (equalityCommutative (binNatToNIsCanonical (a +B b))) (transitivity (applyEquality binNatToN (equalityCommutative (+BIsInherited' a b))) (nToN (binNatToN a +N binNatToN b)))
+binNatToNDistributesPlus : (a b : BinNat) → binNatToN (a +B b) ≡ binNatToN a +N binNatToN b
+binNatToNDistributesPlus a b = transitivity (equalityCommutative (binNatToNIsCanonical (a +B b))) (transitivity (applyEquality binNatToN (equalityCommutative (+BIsInherited' a b))) (nToN (binNatToN a +N binNatToN b)))
 
-  +BAssociative : (a b c : BinNat) → canonical (a +B (b +B c)) ≡ canonical ((a +B b) +B c)
-  +BAssociative a b c rewrite equalityCommutative (+BIsInherited' a (b +B c)) | equalityCommutative (+BIsInherited' (a +B b) c) | binNatToNDistributesPlus a b | binNatToNDistributesPlus b c | equalityCommutative (Semiring.+Associative ℕSemiring (binNatToN a) (binNatToN b) (binNatToN c)) = refl
++BAssociative : (a b c : BinNat) → canonical (a +B (b +B c)) ≡ canonical ((a +B b) +B c)
++BAssociative a b c rewrite equalityCommutative (+BIsInherited' a (b +B c)) | equalityCommutative (+BIsInherited' (a +B b) c) | binNatToNDistributesPlus a b | binNatToNDistributesPlus b c | equalityCommutative (Semiring.+Associative ℕSemiring (binNatToN a) (binNatToN b) (binNatToN c)) = refl
 
-  timesOne : (a b : BinNat) → (canonical b) ≡ (one :: []) → canonical (a *B b) ≡ canonical a
-  timesOne [] b pr = refl
-  timesOne (zero :: a) b pr with inspect (canonical (a *B b))
-  timesOne (zero :: a) b pr | [] with≡ prAB with timesZero'' a b prAB
-  timesOne (zero :: a) b pr | [] with≡ prAB | inl a=0 rewrite a=0 | prAB = refl
-  timesOne (zero :: a) b pr | [] with≡ prAB | inr b=0 = exFalso (nonEmptyNotEmpty (transitivity (equalityCommutative pr) b=0))
-  timesOne (zero :: a) b pr | (ab1 :: abs) with≡ prAB with inspect (canonical a)
-  timesOne (zero :: a) b pr | (ab1 :: abs) with≡ prAB | [] with≡ x = exFalso (nonEmptyNotEmpty (transitivity (equalityCommutative prAB) (timesZero a b x)))
-  timesOne (zero :: a) b pr | (ab1 :: abs) with≡ prAB | (x₁ :: y) with≡ x rewrite prAB | x | timesOne a b pr = applyEquality (zero ::_) (transitivity (equalityCommutative prAB) x)
-  timesOne (one :: a) (zero :: b) pr with canonical b
-  timesOne (one :: a) (zero :: b) () | []
-  timesOne (one :: a) (zero :: b) () | x :: bl
-  timesOne (one :: a) (one :: b) pr rewrite canonicalDistributesPlus (a *B (one :: b)) b | ::Inj pr | +BCommutative (canonical (a *B (one :: b))) [] | timesOne a (one :: b) pr = refl
+timesOne : (a b : BinNat) → (canonical b) ≡ (one :: []) → canonical (a *B b) ≡ canonical a
+timesOne [] b pr = refl
+timesOne (zero :: a) b pr with inspect (canonical (a *B b))
+timesOne (zero :: a) b pr | [] with≡ prAB with timesZero'' a b prAB
+timesOne (zero :: a) b pr | [] with≡ prAB | inl a=0 rewrite a=0 | prAB = refl
+timesOne (zero :: a) b pr | [] with≡ prAB | inr b=0 = exFalso (nonEmptyNotEmpty (transitivity (equalityCommutative pr) b=0))
+timesOne (zero :: a) b pr | (ab1 :: abs) with≡ prAB with inspect (canonical a)
+timesOne (zero :: a) b pr | (ab1 :: abs) with≡ prAB | [] with≡ x = exFalso (nonEmptyNotEmpty (transitivity (equalityCommutative prAB) (timesZero a b x)))
+timesOne (zero :: a) b pr | (ab1 :: abs) with≡ prAB | (x₁ :: y) with≡ x rewrite prAB | x | timesOne a b pr = applyEquality (zero ::_) (transitivity (equalityCommutative prAB) x)
+timesOne (one :: a) (zero :: b) pr with canonical b
+timesOne (one :: a) (zero :: b) () | []
+timesOne (one :: a) (zero :: b) () | x :: bl
+timesOne (one :: a) (one :: b) pr rewrite canonicalDistributesPlus (a *B (one :: b)) b | ::Inj pr | +BCommutative (canonical (a *B (one :: b))) [] | timesOne a (one :: b) pr = refl
 
-  timesZero' : (a b : BinNat) → canonical b ≡ [] → canonical (a *B b) ≡ []
-  timesZero' [] b pr = refl
-  timesZero' (zero :: a) b pr with inspect (canonical (a *B b))
-  timesZero' (zero :: a) b pr | [] with≡ x rewrite x = refl
-  timesZero' (zero :: a) b pr | (ab1 :: abs) with≡ prAB rewrite prAB = exFalso (nonEmptyNotEmpty (transitivity (equalityCommutative prAB) (timesZero' a b pr)))
-  timesZero' (one :: a) b pr rewrite canonicalDistributesPlus (zero :: (a *B b)) b | pr | +BCommutative (canonical (zero :: (a *B b))) [] = ans
-    where
-      ans : canonical (zero :: (a *B b)) ≡ []
-      ans with inspect (canonical (a *B b))
-      ans | [] with≡ x rewrite x = refl
-      ans | (x₁ :: y) with≡ x rewrite x = exFalso (nonEmptyNotEmpty (transitivity (equalityCommutative x) (timesZero' a b pr)))
+timesZero' : (a b : BinNat) → canonical b ≡ [] → canonical (a *B b) ≡ []
+timesZero' [] b pr = refl
+timesZero' (zero :: a) b pr with inspect (canonical (a *B b))
+timesZero' (zero :: a) b pr | [] with≡ x rewrite x = refl
+timesZero' (zero :: a) b pr | (ab1 :: abs) with≡ prAB rewrite prAB = exFalso (nonEmptyNotEmpty (transitivity (equalityCommutative prAB) (timesZero' a b pr)))
+timesZero' (one :: a) b pr rewrite canonicalDistributesPlus (zero :: (a *B b)) b | pr | +BCommutative (canonical (zero :: (a *B b))) [] = ans
+  where
+    ans : canonical (zero :: (a *B b)) ≡ []
+    ans with inspect (canonical (a *B b))
+    ans | [] with≡ x rewrite x = refl
+    ans | (x₁ :: y) with≡ x rewrite x = exFalso (nonEmptyNotEmpty (transitivity (equalityCommutative x) (timesZero' a b pr)))
 
-  canonicalDistributesTimes : (a b : BinNat) → canonical (a *B b) ≡ canonical ((canonical a) *B (canonical b))
-  canonicalDistributesTimes [] b = refl
-  canonicalDistributesTimes (zero :: a) b with inspect (canonical a)
-  canonicalDistributesTimes (zero :: a) b | [] with≡ x rewrite timesZero a b x | x = refl
-  canonicalDistributesTimes (zero :: a) b | (a1 :: as) with≡ prA with inspect (canonical b)
-  canonicalDistributesTimes (zero :: a) b | (a1 :: as) with≡ prA | [] with≡ prB rewrite prA | prB = ans
-    where
-      ans : canonical (zero :: (a *B b)) ≡ canonical (zero :: ((a1 :: as) *B []))
-      ans with inspect (canonical ((a1 :: as) *B []))
-      ans | [] with≡ x rewrite x | timesZero' a b prB = refl
-      ans | (x₁ :: y) with≡ x = exFalso (nonEmptyNotEmpty (equalityCommutative (transitivity (equalityCommutative (timesZero' (a1 :: as) [] refl)) x)))
-  canonicalDistributesTimes (zero :: a) b | (a1 :: as) with≡ prA | (b1 :: bs) with≡ prB with inspect (canonical (a *B b))
-  canonicalDistributesTimes (zero :: a) b | (a1 :: as) with≡ prA | (b1 :: bs) with≡ prB | [] with≡ x with timesZero'' a b x
-  canonicalDistributesTimes (zero :: a) b | (a1 :: as) with≡ prA | (b1 :: bs) with≡ prB | [] with≡ x | inl a=0 = exFalso (nonEmptyNotEmpty (transitivity (equalityCommutative prA) a=0))
-  canonicalDistributesTimes (zero :: a) b | (a1 :: as) with≡ prA | (b1 :: bs) with≡ prB | [] with≡ x | inr b=0 = exFalso (nonEmptyNotEmpty (transitivity (equalityCommutative prB) b=0))
-  canonicalDistributesTimes (zero :: a) b | (a1 :: as) with≡ prA | (b1 :: bs) with≡ prB | (ab1 :: abs) with≡ x rewrite prA | prB | x = ans
-    where
-      ans : zero :: ab1 :: abs ≡ canonical (zero :: ((a1 :: as) *B (b1 :: bs)))
-      ans rewrite equalityCommutative prA | equalityCommutative prB | equalityCommutative (canonicalDistributesTimes a b) | x = refl
-  canonicalDistributesTimes (one :: a) b = transitivity (canonicalDistributesPlus (zero :: (a *B b)) b) (transitivity (transitivity (applyEquality (_+B canonical b) (transitivity (equalityCommutative (canonicalAscends'' (a *B b))) (transitivity (applyEquality (λ i → canonical (zero :: i)) (canonicalDistributesTimes a b)) (canonicalAscends'' (canonical a *B canonical b))))) (applyEquality (λ i → canonical (zero :: (canonical a *B canonical b)) +B i) (canonicalIdempotent b))) (equalityCommutative (canonicalDistributesPlus (zero :: (canonical a *B canonical b)) (canonical b))))
+canonicalDistributesTimes : (a b : BinNat) → canonical (a *B b) ≡ canonical ((canonical a) *B (canonical b))
+canonicalDistributesTimes [] b = refl
+canonicalDistributesTimes (zero :: a) b with inspect (canonical a)
+canonicalDistributesTimes (zero :: a) b | [] with≡ x rewrite timesZero a b x | x = refl
+canonicalDistributesTimes (zero :: a) b | (a1 :: as) with≡ prA with inspect (canonical b)
+canonicalDistributesTimes (zero :: a) b | (a1 :: as) with≡ prA | [] with≡ prB rewrite prA | prB = ans
+  where
+    ans : canonical (zero :: (a *B b)) ≡ canonical (zero :: ((a1 :: as) *B []))
+    ans with inspect (canonical ((a1 :: as) *B []))
+    ans | [] with≡ x rewrite x | timesZero' a b prB = refl
+    ans | (x₁ :: y) with≡ x = exFalso (nonEmptyNotEmpty (equalityCommutative (transitivity (equalityCommutative (timesZero' (a1 :: as) [] refl)) x)))
+canonicalDistributesTimes (zero :: a) b | (a1 :: as) with≡ prA | (b1 :: bs) with≡ prB with inspect (canonical (a *B b))
+canonicalDistributesTimes (zero :: a) b | (a1 :: as) with≡ prA | (b1 :: bs) with≡ prB | [] with≡ x with timesZero'' a b x
+canonicalDistributesTimes (zero :: a) b | (a1 :: as) with≡ prA | (b1 :: bs) with≡ prB | [] with≡ x | inl a=0 = exFalso (nonEmptyNotEmpty (transitivity (equalityCommutative prA) a=0))
+canonicalDistributesTimes (zero :: a) b | (a1 :: as) with≡ prA | (b1 :: bs) with≡ prB | [] with≡ x | inr b=0 = exFalso (nonEmptyNotEmpty (transitivity (equalityCommutative prB) b=0))
+canonicalDistributesTimes (zero :: a) b | (a1 :: as) with≡ prA | (b1 :: bs) with≡ prB | (ab1 :: abs) with≡ x rewrite prA | prB | x = ans
+  where
+    ans : zero :: ab1 :: abs ≡ canonical (zero :: ((a1 :: as) *B (b1 :: bs)))
+    ans rewrite equalityCommutative prA | equalityCommutative prB | equalityCommutative (canonicalDistributesTimes a b) | x = refl
+canonicalDistributesTimes (one :: a) b = transitivity (canonicalDistributesPlus (zero :: (a *B b)) b) (transitivity (transitivity (applyEquality (_+B canonical b) (transitivity (equalityCommutative (canonicalAscends'' (a *B b))) (transitivity (applyEquality (λ i → canonical (zero :: i)) (canonicalDistributesTimes a b)) (canonicalAscends'' (canonical a *B canonical b))))) (applyEquality (λ i → canonical (zero :: (canonical a *B canonical b)) +B i) (canonicalIdempotent b))) (equalityCommutative (canonicalDistributesPlus (zero :: (canonical a *B canonical b)) (canonical b))))
 
-  NToBinNatDistributesPlus : (a b : ℕ) → NToBinNat (a +N b) ≡ NToBinNat a +B NToBinNat b
-  NToBinNatDistributesPlus zero b = refl
-  NToBinNatDistributesPlus (succ a) b with inspect (NToBinNat a)
-  ... | bl with≡ prA with inspect (NToBinNat (a +N b))
-  ... | q with≡ prAB = transitivity (applyEquality incr (NToBinNatDistributesPlus a b)) (incrPullsOut (NToBinNat a) (NToBinNat b))
+NToBinNatDistributesPlus : (a b : ℕ) → NToBinNat (a +N b) ≡ NToBinNat a +B NToBinNat b
+NToBinNatDistributesPlus zero b = refl
+NToBinNatDistributesPlus (succ a) b with inspect (NToBinNat a)
+... | bl with≡ prA with inspect (NToBinNat (a +N b))
+... | q with≡ prAB = transitivity (applyEquality incr (NToBinNatDistributesPlus a b)) (incrPullsOut (NToBinNat a) (NToBinNat b))
 
-  timesCommutative : (a b : BinNat) → canonical (a *B b) ≡ canonical (b *B a)
-  timesCommLemma : (a b : BinNat) → canonical (zero :: (b *B a)) ≡ canonical (b *B (zero :: a))
-  timesCommLemma a b rewrite timesCommutative b (zero :: a) | equalityCommutative (canonicalAscends'' {zero} (b *B a)) | equalityCommutative (canonicalAscends'' {zero} (a *B b)) | timesCommutative b a = refl
+timesCommutative : (a b : BinNat) → canonical (a *B b) ≡ canonical (b *B a)
+timesCommLemma : (a b : BinNat) → canonical (zero :: (b *B a)) ≡ canonical (b *B (zero :: a))
+timesCommLemma a b rewrite timesCommutative b (zero :: a) | equalityCommutative (canonicalAscends'' {zero} (b *B a)) | equalityCommutative (canonicalAscends'' {zero} (a *B b)) | timesCommutative b a = refl
 
-  timesCommutative [] b rewrite timesZero' b [] refl = refl
-  timesCommutative (x :: a) [] rewrite timesZero' (x :: a) [] refl = refl
-  timesCommutative (zero :: as) (zero :: b) rewrite equalityCommutative (canonicalAscends'' {zero} (as *B (zero :: b))) | timesCommutative as (zero :: b) | canonicalAscends'' {zero} (zero :: b *B as) | equalityCommutative (canonicalAscends'' {zero} (b *B (zero :: as))) | timesCommutative b (zero :: as) | canonicalAscends'' {zero} (zero :: (as *B b)) = ans
-    where
-      ans : canonical (zero :: zero :: (b *B as)) ≡ canonical (zero :: zero :: (as *B b))
-      ans rewrite equalityCommutative (canonicalAscends'' {zero} (zero :: (b *B as))) | equalityCommutative (canonicalAscends'' {zero} (b *B as)) | timesCommutative b as | canonicalAscends'' {zero} (as *B b) | canonicalAscends'' {zero} (zero :: (as *B b)) = refl
-  timesCommutative (zero :: as) (one :: b) = transitivity (equalityCommutative (canonicalAscends'' (as *B (one :: b)))) (transitivity (applyEquality (λ i → canonical (zero :: i)) (timesCommutative as (one :: b))) (transitivity (applyEquality (λ i → canonical (zero :: i)) ans) (canonicalAscends'' ((b *B (zero :: as)) +B as))))
-    where
-      ans : canonical ((zero :: (b *B as)) +B as) ≡ canonical ((b *B (zero :: as)) +B as)
-      ans rewrite canonicalDistributesPlus (zero :: (b *B as)) as | canonicalDistributesPlus (b *B (zero :: as)) as = applyEquality (_+B canonical as) (timesCommLemma as b)
-  timesCommutative (one :: as) (zero :: bs) = transitivity (equalityCommutative (canonicalAscends'' ((as *B (zero :: bs)) +B bs))) (transitivity (applyEquality (λ i → canonical (zero :: i)) ans) (canonicalAscends'' (bs *B (one :: as))))
-    where
-      ans : canonical ((as *B (zero :: bs)) +B bs) ≡ canonical (bs *B (one :: as))
-      ans rewrite timesCommutative bs (one :: as) | canonicalDistributesPlus (as *B (zero :: bs)) bs | canonicalDistributesPlus (zero :: (as *B bs)) bs = applyEquality (_+B canonical bs) (equalityCommutative (timesCommLemma bs as))
-  timesCommutative (one :: as) (one :: bs) = applyEquality (one ::_) (transitivity (canonicalDistributesPlus (as *B (one :: bs)) bs) (transitivity (transitivity (applyEquality (_+B canonical bs) (timesCommutative as (one :: bs))) (transitivity ans (equalityCommutative (applyEquality (_+B canonical as) (timesCommutative bs (one :: as)))))) (equalityCommutative (canonicalDistributesPlus (bs *B (one :: as)) as))))
-    where
-      ans : canonical ((zero :: (bs *B as)) +B as) +B canonical bs ≡ canonical ((zero :: (as *B bs)) +B bs) +B canonical as
-      ans rewrite equalityCommutative (canonicalDistributesPlus ((zero :: (bs *B as)) +B as) bs) | equalityCommutative (canonicalDistributesPlus ((zero :: (as *B bs)) +B bs) as) | equalityCommutative (+BAssociative (zero :: (bs *B as)) as bs) | equalityCommutative (+BAssociative (zero :: (as *B bs)) bs as) | canonicalDistributesPlus (zero :: (bs *B as)) (as +B bs) | canonicalDistributesPlus (zero :: (as *B bs)) (bs +B as) | equalityCommutative (canonicalAscends'' {zero} (bs *B as)) | timesCommutative bs as | canonicalAscends'' {zero} (as *B bs) | +BCommutative as bs = refl
+timesCommutative [] b rewrite timesZero' b [] refl = refl
+timesCommutative (x :: a) [] rewrite timesZero' (x :: a) [] refl = refl
+timesCommutative (zero :: as) (zero :: b) rewrite equalityCommutative (canonicalAscends'' {zero} (as *B (zero :: b))) | timesCommutative as (zero :: b) | canonicalAscends'' {zero} (zero :: b *B as) | equalityCommutative (canonicalAscends'' {zero} (b *B (zero :: as))) | timesCommutative b (zero :: as) | canonicalAscends'' {zero} (zero :: (as *B b)) = ans
+  where
+    ans : canonical (zero :: zero :: (b *B as)) ≡ canonical (zero :: zero :: (as *B b))
+    ans rewrite equalityCommutative (canonicalAscends'' {zero} (zero :: (b *B as))) | equalityCommutative (canonicalAscends'' {zero} (b *B as)) | timesCommutative b as | canonicalAscends'' {zero} (as *B b) | canonicalAscends'' {zero} (zero :: (as *B b)) = refl
+timesCommutative (zero :: as) (one :: b) = transitivity (equalityCommutative (canonicalAscends'' (as *B (one :: b)))) (transitivity (applyEquality (λ i → canonical (zero :: i)) (timesCommutative as (one :: b))) (transitivity (applyEquality (λ i → canonical (zero :: i)) ans) (canonicalAscends'' ((b *B (zero :: as)) +B as))))
+  where
+    ans : canonical ((zero :: (b *B as)) +B as) ≡ canonical ((b *B (zero :: as)) +B as)
+    ans rewrite canonicalDistributesPlus (zero :: (b *B as)) as | canonicalDistributesPlus (b *B (zero :: as)) as = applyEquality (_+B canonical as) (timesCommLemma as b)
+timesCommutative (one :: as) (zero :: bs) = transitivity (equalityCommutative (canonicalAscends'' ((as *B (zero :: bs)) +B bs))) (transitivity (applyEquality (λ i → canonical (zero :: i)) ans) (canonicalAscends'' (bs *B (one :: as))))
+  where
+    ans : canonical ((as *B (zero :: bs)) +B bs) ≡ canonical (bs *B (one :: as))
+    ans rewrite timesCommutative bs (one :: as) | canonicalDistributesPlus (as *B (zero :: bs)) bs | canonicalDistributesPlus (zero :: (as *B bs)) bs = applyEquality (_+B canonical bs) (equalityCommutative (timesCommLemma bs as))
+timesCommutative (one :: as) (one :: bs) = applyEquality (one ::_) (transitivity (canonicalDistributesPlus (as *B (one :: bs)) bs) (transitivity (transitivity (applyEquality (_+B canonical bs) (timesCommutative as (one :: bs))) (transitivity ans (equalityCommutative (applyEquality (_+B canonical as) (timesCommutative bs (one :: as)))))) (equalityCommutative (canonicalDistributesPlus (bs *B (one :: as)) as))))
+  where
+    ans : canonical ((zero :: (bs *B as)) +B as) +B canonical bs ≡ canonical ((zero :: (as *B bs)) +B bs) +B canonical as
+    ans rewrite equalityCommutative (canonicalDistributesPlus ((zero :: (bs *B as)) +B as) bs) | equalityCommutative (canonicalDistributesPlus ((zero :: (as *B bs)) +B bs) as) | equalityCommutative (+BAssociative (zero :: (bs *B as)) as bs) | equalityCommutative (+BAssociative (zero :: (as *B bs)) bs as) | canonicalDistributesPlus (zero :: (bs *B as)) (as +B bs) | canonicalDistributesPlus (zero :: (as *B bs)) (bs +B as) | equalityCommutative (canonicalAscends'' {zero} (bs *B as)) | timesCommutative bs as | canonicalAscends'' {zero} (as *B bs) | +BCommutative as bs = refl
 
-  *BIsInherited : (a b : BinNat) → a *Binherit b ≡ canonical (a *B b)
-  *BIsInherited a b = transitivity (applyEquality NToBinNat t) (transitivity (binToBin (canonical (a *B b))) (equalityCommutative (canonicalIdempotent (a *B b))))
-    where
-      ans : (a b : BinNat) → binNatToN a *N binNatToN b ≡ binNatToN (a *B b)
-      ans [] b = refl
-      ans (zero :: a) b rewrite equalityCommutative (ans a b) = equalityCommutative (Semiring.*Associative ℕSemiring 2 (binNatToN a) (binNatToN b))
-      ans (one :: a) b rewrite binNatToNDistributesPlus (zero :: (a *B b)) b | Semiring.commutative ℕSemiring (binNatToN b) ((2 *N (binNatToN a)) *N (binNatToN b)) | equalityCommutative (ans a b) = applyEquality (_+N binNatToN b) (equalityCommutative (Semiring.*Associative ℕSemiring 2 (binNatToN a) (binNatToN b)))
-      t : (binNatToN a *N binNatToN b) ≡ binNatToN (canonical (a *B b))
-      t = transitivity (ans a b) (equalityCommutative (binNatToNIsCanonical (a *B b)))
+*BIsInherited : (a b : BinNat) → a *Binherit b ≡ canonical (a *B b)
+*BIsInherited a b = transitivity (applyEquality NToBinNat t) (transitivity (binToBin (canonical (a *B b))) (equalityCommutative (canonicalIdempotent (a *B b))))
+  where
+    ans : (a b : BinNat) → binNatToN a *N binNatToN b ≡ binNatToN (a *B b)
+    ans [] b = refl
+    ans (zero :: a) b rewrite equalityCommutative (ans a b) = equalityCommutative (Semiring.*Associative ℕSemiring 2 (binNatToN a) (binNatToN b))
+    ans (one :: a) b rewrite binNatToNDistributesPlus (zero :: (a *B b)) b | Semiring.commutative ℕSemiring (binNatToN b) ((2 *N (binNatToN a)) *N (binNatToN b)) | equalityCommutative (ans a b) = applyEquality (_+N binNatToN b) (equalityCommutative (Semiring.*Associative ℕSemiring 2 (binNatToN a) (binNatToN b)))
+    t : (binNatToN a *N binNatToN b) ≡ binNatToN (canonical (a *B b))
+    t = transitivity (ans a b) (equalityCommutative (binNatToNIsCanonical (a *B b)))
diff --git a/ProjectEuler/Problem1.agda b/ProjectEuler/Problem1.agda
new file mode 100644
index 0000000..67e4942
--- /dev/null
+++ b/ProjectEuler/Problem1.agda
@@ -0,0 +1,35 @@
+{-# OPTIONS --warning=error --safe #-}
+
+open import LogicalFormulae
+open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
+open import Numbers.Naturals.Semiring
+open import Numbers.Naturals.Order
+open import Lists.Lists
+open import Numbers.Primes.PrimeNumbers
+open import Decidable.Relations
+open import Numbers.BinaryNaturals.Definition
+open import Numbers.BinaryNaturals.Addition
+
+module ProjectEuler.Problem1 where
+
+numbers<N : (N : ℕ) → List ℕ
+numbers<N zero = []
+numbers<N (succ N) = N :: numbers<N N
+
+filter' : {a b : _} {A : Set a} {f : A → Set b} (decidable : (x : A) → (f x) || (f x → False)) → List A → List A
+filter' {f} decid [] = []
+filter' {f} decid (x :: xs) with decid x
+filter' {f} decid (x :: xs) | inl fx = x :: filter' decid xs
+filter' {f} decid (x :: xs) | inr Notfx = filter' decid xs
+
+filtered : (N : ℕ) → List ℕ
+filtered N = filter' (orDecidable (divisionDecidable 3) (divisionDecidable 5)) (numbers<N N)
+
+ans : ℕ → ℕ
+ans n = binNatToN (fold _+B_ (NToBinNat 0) (map NToBinNat (filtered n)))
+
+t : ans 10 ≡ 23
+t = refl
+
+--q : ans 1000 ≡ 0 -- takes about 15secs for me to reduce the term that fills this hole
+--q = refl