From 264a5e2bd9344308b90c28019fa578418c18f4c7 Mon Sep 17 00:00:00 2001
From: Patrick Stevens <patrick+github@patrickstevens.co.uk>
Date: Thu, 16 Apr 2020 21:58:35 +0100
Subject: [PATCH] Partially ordered ring, at last (#117)

---
 Fields/CauchyCompletion/Archimedean.agda      |   2 +-
 .../PartiallyOrderedRing.agda                 | 165 ++++++++----------
 2 files changed, 76 insertions(+), 91 deletions(-)

diff --git a/Fields/CauchyCompletion/Archimedean.agda b/Fields/CauchyCompletion/Archimedean.agda
index e813719..de5aaa8 100644
--- a/Fields/CauchyCompletion/Archimedean.agda
+++ b/Fields/CauchyCompletion/Archimedean.agda
@@ -22,7 +22,7 @@ module Fields.CauchyCompletion.Archimedean {m n o : _} {A : Set m} {S : Setoid {
 open import Fields.CauchyCompletion.Group order F
 open import Fields.CauchyCompletion.Ring order F
 open import Fields.CauchyCompletion.Comparison order F
---open import Fields.CauchyCompletion.PartiallyOrderedRing order F
+open import Fields.CauchyCompletion.PartiallyOrderedRing order F
 
 --CArchimedean : Archimedean (toGroup CRing CpOrderedRing)
 --CArchimedean = ?
diff --git a/Fields/CauchyCompletion/PartiallyOrderedRing.agda b/Fields/CauchyCompletion/PartiallyOrderedRing.agda
index 49c9990..b87e76e 100644
--- a/Fields/CauchyCompletion/PartiallyOrderedRing.agda
+++ b/Fields/CauchyCompletion/PartiallyOrderedRing.agda
@@ -17,6 +17,7 @@ open import Setoids.Orders.Total.Definition
 open import Functions
 open import LogicalFormulae
 open import Numbers.Naturals.Semiring
+open import Numbers.Naturals.Addition
 open import Numbers.Naturals.Order
 open import Numbers.Naturals.Order.Lemmas
 open import Semirings.Definition
@@ -60,28 +61,28 @@ open import Fields.CauchyCompletion.Setoid order F
 open import Groups.Homomorphisms.Lemmas CInjectionGroupHom
 open import Setoids.Orders.Total.Lemmas (TotallyOrderedRing.total order)
 
-productPositives : (a b : A) → (injection 0R) <Cr a → (injection 0R) <Cr b → (injection 0R) <Cr (a * b)
-productPositives a b record { e = eA ; 0<e = 0<eA ; N = Na ; property = prA } record { e = eB ; 0<e = 0<eB ; N = Nb ; property = prB } = record { e = eA * eB ; 0<e = orderRespectsMultiplication 0<eA 0<eB ; N = Na +N Nb ; property = ans }
-  where
-    ans : (m : ℕ) → Na +N Nb <N m → ((eA * eB) + index (CauchyCompletion.elts (injection 0R)) m) < (a * b)
-    ans m <m = <WellDefined (symmetric (transitive (+WellDefined reflexive (identityOfIndiscernablesRight _∼_ reflexive (indexAndConst 0R m))) identRight)) reflexive (ringMultiplyPositives 0<eA 0<eB (<WellDefined (transitive (+WellDefined reflexive (identityOfIndiscernablesRight _∼_ reflexive (indexAndConst 0R m))) identRight) reflexive (prA m (inequalityShrinkLeft <m))) (<WellDefined (transitive (+WellDefined reflexive (identityOfIndiscernablesRight _∼_ reflexive (indexAndConst 0R m))) identRight) reflexive (prB m (inequalityShrinkRight <m))))
-
-productPositives' : (a b : CauchyCompletion) (interA interB : A) → (0R < interA) → (0R < interB) → (interA r<C a) → (interB r<C b) → (interA * interB) r<C (a *C b)
-productPositives' a b interA interB 0<iA 0<iB record { e = interA' ; 0<e = 0<interA' ; N = Na ; pr = prA } record { e = interB' ; 0<e = 0<interB' ; N = Nb ; pr = prB } = record { e = interA' * interB' ; 0<e = orderRespectsMultiplication 0<interA' 0<interB' ; N = Na +N Nb ; pr = ans }
-  where
-    ans : (m : ℕ) → (Na +N Nb <N m) → ((interA * interB) + (interA' * interB')) < index (CauchyCompletion.elts (a *C b)) m
-    ans m <m rewrite indexAndApply (CauchyCompletion.elts a) (CauchyCompletion.elts b) _*_ {m} = <Transitive (<WellDefined identRight (symmetric *DistributesOver+) (<WellDefined reflexive (+WellDefined *Commutative *Commutative) (<WellDefined reflexive (+WellDefined (symmetric *DistributesOver+) (symmetric *DistributesOver+)) (<WellDefined groupIsAbelian (transitive (transitive groupIsAbelian (transitive (symmetric +Associative) (+WellDefined *Commutative (transitive groupIsAbelian (transitive (+WellDefined reflexive *Commutative) (symmetric +Associative)))))) +Associative) (orderRespectsAddition (<WellDefined identRight reflexive (ringAddInequalities (orderRespectsMultiplication 0<iB 0<interA') (orderRespectsMultiplication 0<interB' 0<iA))) ((interA * interB) + (interA' * interB'))))))) (ringMultiplyPositives (<WellDefined identRight reflexive (ringAddInequalities 0<iA 0<interA')) (<WellDefined identRight reflexive (ringAddInequalities 0<iB 0<interB')) (prA m (inequalityShrinkLeft <m)) (prB m (inequalityShrinkRight <m)))
-
-<COrderRespectsMultiplication : (a b : CauchyCompletion) → (injection 0R <C a) → (injection 0R <C b) → (injection 0R <C (a *C b))
-<COrderRespectsMultiplication a b record { i = interA ; a<i = 0<interA ; i<b = interA<a } record { i = interB ; a<i = 0<interB ; i<b = interB<b } = record { i = interA * interB ; a<i = productPositives interA interB 0<interA 0<interB ; i<b = productPositives' a b interA interB (<CCollapsesL 0R _ 0<interA) (<CCollapsesL 0R _ 0<interB) interA<a interB<b }
-
-cOrderRespectsAdditionLeft' : (a : CauchyCompletion) (b : A) (c : A) → (a <Cr b) → (a +C injection c) <C (injection b +C injection c)
-cOrderRespectsAdditionLeft' a b c record { e = e ; 0<e = 0<e ; N = N ; property = pr } = <CWellDefined {a +C injection c} {a +C injection c} {injection (b + c)} {(injection b) +C (injection c)} (Equivalence.reflexive (Setoid.eq cauchyCompletionSetoid) {a +C injection c}) (GroupHom.groupHom (RingHom.groupHom CInjectionRingHom)) (<CRelaxR (record { e = e ; 0<e = 0<e ; N = N ; property = λ m N<m → <WellDefined (transitive (symmetric +Associative) (+WellDefined reflexive (ans m))) reflexive (orderRespectsAddition (pr m N<m) c) }))
-  where
-    ans : (m : ℕ) → (index (CauchyCompletion.elts a) m + c) ∼ index (apply _+_ (CauchyCompletion.elts a) (constSequence c)) m
-    ans m rewrite indexAndApply (CauchyCompletion.elts a) (constSequence c) _+_ {m} | indexAndConst c m = reflexive
-
 private
+  productPositives : (a b : A) → (injection 0R) <Cr a → (injection 0R) <Cr b → (injection 0R) <Cr (a * b)
+  productPositives a b record { e = eA ; 0<e = 0<eA ; N = Na ; property = prA } record { e = eB ; 0<e = 0<eB ; N = Nb ; property = prB } = record { e = eA * eB ; 0<e = orderRespectsMultiplication 0<eA 0<eB ; N = Na +N Nb ; property = ans }
+    where
+      ans : (m : ℕ) → Na +N Nb <N m → ((eA * eB) + index (CauchyCompletion.elts (injection 0R)) m) < (a * b)
+      ans m <m = <WellDefined (symmetric (transitive (+WellDefined reflexive (identityOfIndiscernablesRight _∼_ reflexive (indexAndConst 0R m))) identRight)) reflexive (ringMultiplyPositives 0<eA 0<eB (<WellDefined (transitive (+WellDefined reflexive (identityOfIndiscernablesRight _∼_ reflexive (indexAndConst 0R m))) identRight) reflexive (prA m (inequalityShrinkLeft <m))) (<WellDefined (transitive (+WellDefined reflexive (identityOfIndiscernablesRight _∼_ reflexive (indexAndConst 0R m))) identRight) reflexive (prB m (inequalityShrinkRight <m))))
+
+  productPositives' : (a b : CauchyCompletion) (interA interB : A) → (0R < interA) → (0R < interB) → (interA r<C a) → (interB r<C b) → (interA * interB) r<C (a *C b)
+  productPositives' a b interA interB 0<iA 0<iB record { e = interA' ; 0<e = 0<interA' ; N = Na ; pr = prA } record { e = interB' ; 0<e = 0<interB' ; N = Nb ; pr = prB } = record { e = interA' * interB' ; 0<e = orderRespectsMultiplication 0<interA' 0<interB' ; N = Na +N Nb ; pr = ans }
+    where
+      ans : (m : ℕ) → (Na +N Nb <N m) → ((interA * interB) + (interA' * interB')) < index (CauchyCompletion.elts (a *C b)) m
+      ans m <m rewrite indexAndApply (CauchyCompletion.elts a) (CauchyCompletion.elts b) _*_ {m} = <Transitive (<WellDefined identRight (symmetric *DistributesOver+) (<WellDefined reflexive (+WellDefined *Commutative *Commutative) (<WellDefined reflexive (+WellDefined (symmetric *DistributesOver+) (symmetric *DistributesOver+)) (<WellDefined groupIsAbelian (transitive (transitive groupIsAbelian (transitive (symmetric +Associative) (+WellDefined *Commutative (transitive groupIsAbelian (transitive (+WellDefined reflexive *Commutative) (symmetric +Associative)))))) +Associative) (orderRespectsAddition (<WellDefined identRight reflexive (ringAddInequalities (orderRespectsMultiplication 0<iB 0<interA') (orderRespectsMultiplication 0<interB' 0<iA))) ((interA * interB) + (interA' * interB'))))))) (ringMultiplyPositives (<WellDefined identRight reflexive (ringAddInequalities 0<iA 0<interA')) (<WellDefined identRight reflexive (ringAddInequalities 0<iB 0<interB')) (prA m (inequalityShrinkLeft <m)) (prB m (inequalityShrinkRight <m)))
+
+  <COrderRespectsMultiplication : (a b : CauchyCompletion) → (injection 0R <C a) → (injection 0R <C b) → (injection 0R <C (a *C b))
+  <COrderRespectsMultiplication a b record { i = interA ; a<i = 0<interA ; i<b = interA<a } record { i = interB ; a<i = 0<interB ; i<b = interB<b } = record { i = interA * interB ; a<i = productPositives interA interB 0<interA 0<interB ; i<b = productPositives' a b interA interB (<CCollapsesL 0R _ 0<interA) (<CCollapsesL 0R _ 0<interB) interA<a interB<b }
+
+  cOrderRespectsAdditionLeft' : (a : CauchyCompletion) (b : A) (c : A) → (a <Cr b) → (a +C injection c) <C (injection b +C injection c)
+  cOrderRespectsAdditionLeft' a b c record { e = e ; 0<e = 0<e ; N = N ; property = pr } = <CWellDefined {a +C injection c} {a +C injection c} {injection (b + c)} {(injection b) +C (injection c)} (Equivalence.reflexive (Setoid.eq cauchyCompletionSetoid) {a +C injection c}) (GroupHom.groupHom (RingHom.groupHom CInjectionRingHom)) (<CRelaxR (record { e = e ; 0<e = 0<e ; N = N ; property = λ m N<m → <WellDefined (transitive (symmetric +Associative) (+WellDefined reflexive (ans m))) reflexive (orderRespectsAddition (pr m N<m) c) }))
+    where
+      ans : (m : ℕ) → (index (CauchyCompletion.elts a) m + c) ∼ index (apply _+_ (CauchyCompletion.elts a) (constSequence c)) m
+      ans m rewrite indexAndApply (CauchyCompletion.elts a) (constSequence c) _+_ {m} | indexAndConst c m = reflexive
+
   l1 : (a : A) (b : CauchyCompletion) → a r<C b → 0R r<C (b +C injection (inverse a))
   l1 a b record { e = e ; 0<e = 0<e ; N = N ; pr = pr } = record { e = e ; 0<e = 0<e ; N = N ; pr = λ m N<m → <WellDefined (transitive groupIsAbelian (transitive +Associative (+WellDefined invLeft reflexive))) (ans m) (orderRespectsAddition (pr m N<m) (inverse a)) }
     where
@@ -137,37 +138,36 @@ private
   invInj : (i : A) → Setoid._∼_ cauchyCompletionSetoid (injection (inverse i) +C injection i) (injection 0R)
   invInj i = Equivalence.transitive (Setoid.eq cauchyCompletionSetoid) {record { converges = CauchyCompletion.converges (injection (inverse i) +C injection i) }} {record { converges = CauchyCompletion.converges ((-C (injection i)) +C injection i) }} {record { converges = CauchyCompletion.converges (injection 0R) }} (Group.+WellDefined CGroup {record { converges = CauchyCompletion.converges (injection (inverse i)) }} {record { converges = CauchyCompletion.converges (injection i)}} {record { converges = CauchyCompletion.converges (-C (injection i)) }} {record { converges = CauchyCompletion.converges (injection i) }} homRespectsInverse (Equivalence.reflexive (Setoid.eq cauchyCompletionSetoid) {record { converges = CauchyCompletion.converges (injection i) }})) (Group.invLeft CGroup {injection i})
 
+  cOrderMove : (a b : A) (c : CauchyCompletion) → (injection a +C c) <Cr b → a r<C (injection b +C (-C c))
+  cOrderMove a b c record { e = e ; 0<e = 0<e ; N = N ; property = property } = record { e = e ; 0<e = 0<e ; N = N ; pr = λ m N<m → <WellDefined (transitive (symmetric +Associative) (transitive (+WellDefined reflexive (transitive (+WellDefined (identityOfIndiscernablesRight _∼_ reflexive (indexAndApply (CauchyCompletion.elts (injection a)) (CauchyCompletion.elts c) _+_ {m})) reflexive) (transitive (symmetric +Associative) (transitive (+WellDefined (identityOfIndiscernablesRight _∼_ reflexive (indexAndConst a m)) invRight) identRight)))) groupIsAbelian)) (transitive (+WellDefined (identityOfIndiscernablesLeft _∼_ reflexive (indexAndConst b m)) (identityOfIndiscernablesRight _∼_ reflexive (mapAndIndex (CauchyCompletion.elts c) inverse m))) (identityOfIndiscernablesLeft _∼_ reflexive (indexAndApply (CauchyCompletion.elts (injection b)) (CauchyCompletion.elts (-C c)) _+_ {m}))) (orderRespectsAddition (property m N<m) (inverse (index (CauchyCompletion.elts c) m))) }
 
-cOrderMove : (a b : A) (c : CauchyCompletion) → (injection a +C c) <Cr b → a r<C (injection b +C (-C c))
-cOrderMove a b c record { e = e ; 0<e = 0<e ; N = N ; property = property } = record { e = e ; 0<e = 0<e ; N = N ; pr = λ m N<m → <WellDefined (transitive (symmetric +Associative) (transitive (+WellDefined reflexive (transitive (+WellDefined (identityOfIndiscernablesRight _∼_ reflexive (indexAndApply (CauchyCompletion.elts (injection a)) (CauchyCompletion.elts c) _+_ {m})) reflexive) (transitive (symmetric +Associative) (transitive (+WellDefined (identityOfIndiscernablesRight _∼_ reflexive (indexAndConst a m)) invRight) identRight)))) groupIsAbelian)) (transitive (+WellDefined (identityOfIndiscernablesLeft _∼_ reflexive (indexAndConst b m)) (identityOfIndiscernablesRight _∼_ reflexive (mapAndIndex (CauchyCompletion.elts c) inverse m))) (identityOfIndiscernablesLeft _∼_ reflexive (indexAndApply (CauchyCompletion.elts (injection b)) (CauchyCompletion.elts (-C c)) _+_ {m}))) (orderRespectsAddition (property m N<m) (inverse (index (CauchyCompletion.elts c) m))) }
+  cOrderMove' : (a b : A) (c : CauchyCompletion) → (injection a +C (-C c)) <Cr b → a r<C (injection b +C c)
+  cOrderMove' a b c pr = r<CWellDefinedRight _ _ _ (Group.+WellDefined CGroup {record { converges = CauchyCompletion.converges (injection b) }} {record { converges = CauchyCompletion.converges (-C (-C c)) }} {record { converges = CauchyCompletion.converges (injection b) }} {record {converges = CauchyCompletion.converges c }} (Equivalence.reflexive (Setoid.eq cauchyCompletionSetoid) {record { converges = CauchyCompletion.converges (injection b) }}) (invTwice CGroup record { converges = CauchyCompletion.converges c })) (cOrderMove a b (-C c) pr)
 
-cOrderMove' : (a b : A) (c : CauchyCompletion) → (injection a +C (-C c)) <Cr b → a r<C (injection b +C c)
-cOrderMove' a b c pr = r<CWellDefinedRight _ _ _ (Group.+WellDefined CGroup {record { converges = CauchyCompletion.converges (injection b) }} {record { converges = CauchyCompletion.converges (-C (-C c)) }} {record { converges = CauchyCompletion.converges (injection b) }} {record {converges = CauchyCompletion.converges c }} (Equivalence.reflexive (Setoid.eq cauchyCompletionSetoid) {record { converges = CauchyCompletion.converges (injection b) }}) (invTwice CGroup record { converges = CauchyCompletion.converges c })) (cOrderMove a b (-C c) pr)
+  cOrderMove'' : (a : CauchyCompletion) (b c : A) → (a +C (-C injection b)) <Cr c → a <Cr (b + c)
+  cOrderMove'' a b c record { e = e ; 0<e = 0<e ; N = N ; property = property } = record { e = e ; 0<e = 0<e ; N = N ; property = λ m N<m → <WellDefined (transitive (symmetric +Associative) (+WellDefined reflexive (transitive (+WellDefined (identityOfIndiscernablesRight _∼_ reflexive (indexAndApply (CauchyCompletion.elts a) _ _+_ {m})) reflexive) (transitive (transitive (symmetric +Associative) (+WellDefined reflexive (transitive (+WellDefined (transitive (identityOfIndiscernablesLeft _∼_ reflexive (mapAndIndex _ inverse m)) (inverseWellDefined additiveGroup (identityOfIndiscernablesRight _∼_ reflexive (indexAndConst b m)))) reflexive) invLeft))) identRight)))) groupIsAbelian (orderRespectsAddition (property m N<m) b) }
 
-cOrderMove'' : (a : CauchyCompletion) (b c : A) → (a +C (-C injection b)) <Cr c → a <Cr (b + c)
-cOrderMove'' a b c record { e = e ; 0<e = 0<e ; N = N ; property = property } = record { e = e ; 0<e = 0<e ; N = N ; property = λ m N<m → <WellDefined (transitive (symmetric +Associative) (+WellDefined reflexive (transitive (+WellDefined (identityOfIndiscernablesRight _∼_ reflexive (indexAndApply (CauchyCompletion.elts a) _ _+_ {m})) reflexive) (transitive (transitive (symmetric +Associative) (+WellDefined reflexive (transitive (+WellDefined (transitive (identityOfIndiscernablesLeft _∼_ reflexive (mapAndIndex _ inverse m)) (inverseWellDefined additiveGroup (identityOfIndiscernablesRight _∼_ reflexive (indexAndConst b m)))) reflexive) invLeft))) identRight)))) groupIsAbelian (orderRespectsAddition (property m N<m) b) }
+  cOrderRespectsAdditionLeft'' : (a b : A) (c : CauchyCompletion) → (a < b) → (injection a +C c) <C (injection b +C c)
+  cOrderRespectsAdditionLeft'' a b c a<b with halve charNot2 (b + inverse a)
+  ... | b-a/2 , prDiff with approximateAbove c b-a/2 (halvePositive' prDiff (moveInequality a<b))
+  ... | aboveC , (c<aboveC ,, aboveC-C<e) = record { i = a + aboveC ; a<i = <CRelaxR' (SetoidPartialOrder.<WellDefined <COrder (Ring.groupIsAbelian CRing {record { converges = CauchyCompletion.converges c }} {record { converges = CauchyCompletion.converges (injection a) }}) (Equivalence.transitive (Setoid.eq cauchyCompletionSetoid) {record { converges = CauchyCompletion.converges (injection aboveC +C injection a) }} {record { converges = CauchyCompletion.converges (injection a +C injection aboveC) }} {record { converges = CauchyCompletion.converges (injection (a + aboveC)) }} (Ring.groupIsAbelian CRing {record { converges = CauchyCompletion.converges (injection aboveC) }} {record { converges = CauchyCompletion.converges (injection a) }}) (Equivalence.symmetric (Setoid.eq cauchyCompletionSetoid) {record { converges = CauchyCompletion.converges (injection (a + aboveC)) }} {record { converges = CauchyCompletion.converges (injection a +C injection aboveC) }} (GroupHom.groupHom CInjectionGroupHom))) (cOrderRespectsAdditionLeft' c aboveC a c<aboveC)) ; i<b = cOrderMove' _ _ _ (<CRelaxR' (<CTransitive (<CRelaxR t) (<CInherited u))) }
+    where
+      g : ((injection aboveC +C (-C c)) +C injection a) <C ((injection b-a/2) +C (injection a))
+      g = cOrderRespectsAdditionLeft' _ _ a (<CRelaxR' aboveC-C<e)
+      g' : ((injection aboveC +C (-C c)) +C injection a) <C (injection (b-a/2 + a))
+      g' = <CWellDefined (Equivalence.reflexive (Setoid.eq cauchyCompletionSetoid) {record { converges = CauchyCompletion.converges ((injection aboveC +C (-C c)) +C injection a) }}) (Equivalence.symmetric (Setoid.eq cauchyCompletionSetoid) {record { converges = CauchyCompletion.converges (injection (b-a/2 + a)) }} {record { converges = CauchyCompletion.converges (injection b-a/2 +C injection a) }} (GroupHom.groupHom CInjectionGroupHom)) g
+      t : (injection (a + aboveC) +C (-C c)) <Cr (b-a/2 + a)
+      t = <CRelaxR' (<CWellDefined (Equivalence.transitive (Setoid.eq cauchyCompletionSetoid) {record { converges = CauchyCompletion.converges (((injection aboveC) +C (-C c)) +C injection a) }} {record { converges = CauchyCompletion.converges (injection a +C ((injection aboveC) +C (-C c))) }} {record { converges = CauchyCompletion.converges (injection (a + aboveC) +C (-C c)) }} (Ring.groupIsAbelian CRing {record { converges = CauchyCompletion.converges (injection aboveC +C (-C c)) }} {record { converges = CauchyCompletion.converges (injection a) }}) (Equivalence.transitive (Setoid.eq cauchyCompletionSetoid) {record { converges = CauchyCompletion.converges (injection a +C ((injection aboveC) +C (-C c))) }} {record { converges = CauchyCompletion.converges (((injection a) +C (injection aboveC)) +C (-C c)) }} {record { converges = CauchyCompletion.converges ((injection (a + aboveC)) +C (-C c)) }} (Group.+Associative CGroup {record { converges = CauchyCompletion.converges (injection a) }} {record { converges = CauchyCompletion.converges (injection aboveC) }} {record { converges = CauchyCompletion.converges (-C c) }}) (Group.+WellDefined CGroup {record { converges = CauchyCompletion.converges (injection a +C injection aboveC) }} {record { converges = CauchyCompletion.converges (-C c) }} {record { converges = CauchyCompletion.converges (injection (a + aboveC)) }} {record { converges = CauchyCompletion.converges (-C c) }} (Equivalence.symmetric (Setoid.eq cauchyCompletionSetoid) {record { converges = CauchyCompletion.converges (injection (a + aboveC)) }} {record { converges = CauchyCompletion.converges (injection a +C injection aboveC) }} (GroupHom.groupHom CInjectionGroupHom)) (Equivalence.reflexive (Setoid.eq cauchyCompletionSetoid) {record { converges = CauchyCompletion.converges (-C c)}})))) (Equivalence.reflexive (Setoid.eq cauchyCompletionSetoid) {record { converges = CauchyCompletion.converges (injection (b-a/2 + a)) }}) g')
+      lemm : 0R < b-a/2
+      lemm = halvePositive' prDiff (moveInequality a<b)
+      u : (b-a/2 + a) < b
+      u = <WellDefined (transitive (+WellDefined (symmetric prDiff) reflexive) (transitive groupIsAbelian (transitive +Associative (transitive (+WellDefined (transitive (symmetric +Associative) (transitive (+WellDefined reflexive invLeft) identRight)) reflexive) groupIsAbelian)))) (transitive (symmetric +Associative) (transitive (+WellDefined reflexive invLeft) identRight)) (orderRespectsAddition (<WellDefined identLeft (transitive (transitive +Associative (transitive (+WellDefined (transitive groupIsAbelian (+WellDefined reflexive (symmetric (invTwice additiveGroup b-a/2)))) reflexive) (symmetric +Associative))) (+WellDefined reflexive (symmetric (invContravariant additiveGroup)))) (orderRespectsAddition lemm (b + inverse a))) (a + inverse b-a/2))
 
-cOrderRespectsAdditionLeft'' : (a b : A) (c : CauchyCompletion) → (a < b) → (injection a +C c) <C (injection b +C c)
-cOrderRespectsAdditionLeft'' a b c a<b with halve charNot2 (b + inverse a)
-... | b-a/2 , prDiff with approximateAbove c b-a/2 (halvePositive' prDiff (moveInequality a<b))
-... | aboveC , (c<aboveC ,, aboveC-C<e) = record { i = a + aboveC ; a<i = <CRelaxR' (SetoidPartialOrder.<WellDefined <COrder (Ring.groupIsAbelian CRing {record { converges = CauchyCompletion.converges c }} {record { converges = CauchyCompletion.converges (injection a) }}) (Equivalence.transitive (Setoid.eq cauchyCompletionSetoid) {record { converges = CauchyCompletion.converges (injection aboveC +C injection a) }} {record { converges = CauchyCompletion.converges (injection a +C injection aboveC) }} {record { converges = CauchyCompletion.converges (injection (a + aboveC)) }} (Ring.groupIsAbelian CRing {record { converges = CauchyCompletion.converges (injection aboveC) }} {record { converges = CauchyCompletion.converges (injection a) }}) (Equivalence.symmetric (Setoid.eq cauchyCompletionSetoid) {record { converges = CauchyCompletion.converges (injection (a + aboveC)) }} {record { converges = CauchyCompletion.converges (injection a +C injection aboveC) }} (GroupHom.groupHom CInjectionGroupHom))) (cOrderRespectsAdditionLeft' c aboveC a c<aboveC)) ; i<b = cOrderMove' _ _ _ (<CRelaxR' (<CTransitive (<CRelaxR t) (<CInherited u))) }
-  where
-    g : ((injection aboveC +C (-C c)) +C injection a) <C ((injection b-a/2) +C (injection a))
-    g = cOrderRespectsAdditionLeft' _ _ a (<CRelaxR' aboveC-C<e)
-    g' : ((injection aboveC +C (-C c)) +C injection a) <C (injection (b-a/2 + a))
-    g' = <CWellDefined (Equivalence.reflexive (Setoid.eq cauchyCompletionSetoid) {record { converges = CauchyCompletion.converges ((injection aboveC +C (-C c)) +C injection a) }}) (Equivalence.symmetric (Setoid.eq cauchyCompletionSetoid) {record { converges = CauchyCompletion.converges (injection (b-a/2 + a)) }} {record { converges = CauchyCompletion.converges (injection b-a/2 +C injection a) }} (GroupHom.groupHom CInjectionGroupHom)) g
-    t : (injection (a + aboveC) +C (-C c)) <Cr (b-a/2 + a)
-    t = <CRelaxR' (<CWellDefined (Equivalence.transitive (Setoid.eq cauchyCompletionSetoid) {record { converges = CauchyCompletion.converges (((injection aboveC) +C (-C c)) +C injection a) }} {record { converges = CauchyCompletion.converges (injection a +C ((injection aboveC) +C (-C c))) }} {record { converges = CauchyCompletion.converges (injection (a + aboveC) +C (-C c)) }} (Ring.groupIsAbelian CRing {record { converges = CauchyCompletion.converges (injection aboveC +C (-C c)) }} {record { converges = CauchyCompletion.converges (injection a) }}) (Equivalence.transitive (Setoid.eq cauchyCompletionSetoid) {record { converges = CauchyCompletion.converges (injection a +C ((injection aboveC) +C (-C c))) }} {record { converges = CauchyCompletion.converges (((injection a) +C (injection aboveC)) +C (-C c)) }} {record { converges = CauchyCompletion.converges ((injection (a + aboveC)) +C (-C c)) }} (Group.+Associative CGroup {record { converges = CauchyCompletion.converges (injection a) }} {record { converges = CauchyCompletion.converges (injection aboveC) }} {record { converges = CauchyCompletion.converges (-C c) }}) (Group.+WellDefined CGroup {record { converges = CauchyCompletion.converges (injection a +C injection aboveC) }} {record { converges = CauchyCompletion.converges (-C c) }} {record { converges = CauchyCompletion.converges (injection (a + aboveC)) }} {record { converges = CauchyCompletion.converges (-C c) }} (Equivalence.symmetric (Setoid.eq cauchyCompletionSetoid) {record { converges = CauchyCompletion.converges (injection (a + aboveC)) }} {record { converges = CauchyCompletion.converges (injection a +C injection aboveC) }} (GroupHom.groupHom CInjectionGroupHom)) (Equivalence.reflexive (Setoid.eq cauchyCompletionSetoid) {record { converges = CauchyCompletion.converges (-C c)}})))) (Equivalence.reflexive (Setoid.eq cauchyCompletionSetoid) {record { converges = CauchyCompletion.converges (injection (b-a/2 + a)) }}) g')
-    lemm : 0R < b-a/2
-    lemm = halvePositive' prDiff (moveInequality a<b)
-    u : (b-a/2 + a) < b
-    u = <WellDefined (transitive (+WellDefined (symmetric prDiff) reflexive) (transitive groupIsAbelian (transitive +Associative (transitive (+WellDefined (transitive (symmetric +Associative) (transitive (+WellDefined reflexive invLeft) identRight)) reflexive) groupIsAbelian)))) (transitive (symmetric +Associative) (transitive (+WellDefined reflexive invLeft) identRight)) (orderRespectsAddition (<WellDefined identLeft (transitive (transitive +Associative (transitive (+WellDefined (transitive groupIsAbelian (+WellDefined reflexive (symmetric (invTwice additiveGroup b-a/2)))) reflexive) (symmetric +Associative))) (+WellDefined reflexive (symmetric (invContravariant additiveGroup)))) (orderRespectsAddition lemm (b + inverse a))) (a + inverse b-a/2))
+  cOrderRespectsAdditionLeft''Flip : (a b : A) (c : CauchyCompletion) → (a < b) → (c +C injection a) <C (c +C injection b)
+  cOrderRespectsAdditionLeft''Flip a b c a<b = <CWellDefined ((Ring.groupIsAbelian CRing {record { converges = CauchyCompletion.converges (injection a) }} {record { converges = CauchyCompletion.converges c }})) (Ring.groupIsAbelian CRing {record { converges = CauchyCompletion.converges (injection b) }} {record { converges = CauchyCompletion.converges c }}) (cOrderRespectsAdditionLeft'' a b c a<b)
 
-cOrderRespectsAdditionLeft''Flip : (a b : A) (c : CauchyCompletion) → (a < b) → (c +C injection a) <C (c +C injection b)
-cOrderRespectsAdditionLeft''Flip a b c a<b = <CWellDefined ((Ring.groupIsAbelian CRing {record { converges = CauchyCompletion.converges (injection a) }} {record { converges = CauchyCompletion.converges c }})) (Ring.groupIsAbelian CRing {record { converges = CauchyCompletion.converges (injection b) }} {record { converges = CauchyCompletion.converges c }}) (cOrderRespectsAdditionLeft'' a b c a<b)
-
-cOrderRespectsAdditionLeft''' : (a b : CauchyCompletion) (c : A) → (a <C b) → (a +C injection c) <C (b +C injection c)
-cOrderRespectsAdditionLeft''' a b c record { i = i ; a<i = a<i ; i<b = i<b } = <CTransitive (cOrderRespectsAdditionLeft' a i c a<i) (<CWellDefined (Equivalence.transitive (Setoid.eq cauchyCompletionSetoid) {record { converges = CauchyCompletion.converges (injection (c + i)) }} {record { converges = CauchyCompletion.converges (injection c +C injection i) }} {record { converges = CauchyCompletion.converges (injection i +C injection c) }} (GroupHom.groupHom CInjectionGroupHom) (Ring.groupIsAbelian CRing {record { converges = CauchyCompletion.converges (injection c) }} {record { converges = CauchyCompletion.converges (injection i) }})) (Ring.groupIsAbelian CRing {record { converges = CauchyCompletion.converges (injection c) }} {record { converges = CauchyCompletion.converges b }}) (flip<C' {record { converges = CauchyCompletion.converges (injection (c + i)) }} {record { converges = CauchyCompletion.converges (injection c +C b) }} (<CWellDefined (Equivalence.transitive (Setoid.eq cauchyCompletionSetoid) {record { converges = CauchyCompletion.converges ((-C b) +C injection (inverse c)) }} {record { converges = CauchyCompletion.converges ((-C b) +C (-C (injection c))) }} {record { converges = CauchyCompletion.converges (-C (injection c +C b)) }} (Group.+WellDefined CGroup {record { converges = CauchyCompletion.converges (-C b) }} {record { converges = CauchyCompletion.converges (injection (inverse c)) }} {record { converges = CauchyCompletion.converges (-C b) }} {record { converges = CauchyCompletion.converges (-C (injection c)) }} (Equivalence.reflexive (Setoid.eq cauchyCompletionSetoid) {record { converges = CauchyCompletion.converges (-C b) }}) homRespectsInverse) (Equivalence.symmetric (Setoid.eq cauchyCompletionSetoid) {record { converges = CauchyCompletion.converges (-C (injection c +C b)) }} {record { converges = CauchyCompletion.converges ((-C b) +C (-C (injection c))) }} (invContravariant CGroup {record { converges = CauchyCompletion.converges (injection c) }} {record { converges = CauchyCompletion.converges b }}))) homRespectsInverse' (cOrderRespectsAdditionLeft' (-C b) (inverse i) (inverse c) (flipR<C i<b)))))
+  cOrderRespectsAdditionLeft''' : (a b : CauchyCompletion) (c : A) → (a <C b) → (a +C injection c) <C (b +C injection c)
+  cOrderRespectsAdditionLeft''' a b c record { i = i ; a<i = a<i ; i<b = i<b } = <CTransitive (cOrderRespectsAdditionLeft' a i c a<i) (<CWellDefined (Equivalence.transitive (Setoid.eq cauchyCompletionSetoid) {record { converges = CauchyCompletion.converges (injection (c + i)) }} {record { converges = CauchyCompletion.converges (injection c +C injection i) }} {record { converges = CauchyCompletion.converges (injection i +C injection c) }} (GroupHom.groupHom CInjectionGroupHom) (Ring.groupIsAbelian CRing {record { converges = CauchyCompletion.converges (injection c) }} {record { converges = CauchyCompletion.converges (injection i) }})) (Ring.groupIsAbelian CRing {record { converges = CauchyCompletion.converges (injection c) }} {record { converges = CauchyCompletion.converges b }}) (flip<C' {record { converges = CauchyCompletion.converges (injection (c + i)) }} {record { converges = CauchyCompletion.converges (injection c +C b) }} (<CWellDefined (Equivalence.transitive (Setoid.eq cauchyCompletionSetoid) {record { converges = CauchyCompletion.converges ((-C b) +C injection (inverse c)) }} {record { converges = CauchyCompletion.converges ((-C b) +C (-C (injection c))) }} {record { converges = CauchyCompletion.converges (-C (injection c +C b)) }} (Group.+WellDefined CGroup {record { converges = CauchyCompletion.converges (-C b) }} {record { converges = CauchyCompletion.converges (injection (inverse c)) }} {record { converges = CauchyCompletion.converges (-C b) }} {record { converges = CauchyCompletion.converges (-C (injection c)) }} (Equivalence.reflexive (Setoid.eq cauchyCompletionSetoid) {record { converges = CauchyCompletion.converges (-C b) }}) homRespectsInverse) (Equivalence.symmetric (Setoid.eq cauchyCompletionSetoid) {record { converges = CauchyCompletion.converges (-C (injection c +C b)) }} {record { converges = CauchyCompletion.converges ((-C b) +C (-C (injection c))) }} (invContravariant CGroup {record { converges = CauchyCompletion.converges (injection c) }} {record { converges = CauchyCompletion.converges b }}))) homRespectsInverse' (cOrderRespectsAdditionLeft' (-C b) (inverse i) (inverse c) (flipR<C i<b)))))
 
 {-
 
@@ -176,60 +176,45 @@ Have c < a- + c, by cOrderRespectsAdditionLeft''
 Have a- + c < a+ + c     by cOrderRespectsAdditionLeft''
   so a- + c < K < a+ + c
 
-
 -}
 
---cOrderRespectsAdditionLeft'' : (a b : A) (c : CauchyCompletion) → (a < b) → (injection a +C c) <C (injection b +C c)
---cOrderRespectsAdditionLeft''' : (a b : CauchyCompletion) (c : A) → (a <C b) → (a +C injection c) <C (b +C injection c)
-cOrderRespectsAdditionRightZero : (a : CauchyCompletion) → (0R r<C a) → (c : CauchyCompletion) → c <C (a +C c)
-cOrderRespectsAdditionRightZero a record { e = e ; 0<e = 0<e ; N = N1 ; pr = pr } c with halve charNot2 e
-... | e/2 , prE/2 with halve charNot2 e/2
-... | e/4 , prE/4 with halve charNot2 e/4
-... | e/8 , prE/8 with approximateAbove c e/4 (halvePositive' prE/4 (halvePositive' prE/2 0<e))
-... | c' , (c<c' ,, c'-c<e/4) with approximateBelow c e/8 (halvePositive' prE/8 (halvePositive' prE/4 (halvePositive' prE/2 0<e)))
-... | cB , (record { e = f ; 0<e = 0<f ; N = N2 ; pr = pr2 } ,, c-cB<e/8) = record { i = c' + e/4 ; a<i = <CRelaxR' (<CTransitive (<CRelaxR c<c') (<CInherited (<WellDefined identLeft groupIsAbelian (orderRespectsAddition (halvePositive' prE/4 (halvePositive' prE/2 0<e)) c')))) ; i<b = record { e = e/4 ; 0<e = halvePositive' prE/4 (halvePositive' prE/2 0<e) ; N = N ; pr = λ m N<m → {!!} } }
-  where
-    N = TotalOrder.max ℕTotalOrder N1 N2
-    3e/4<e : ((e/4 + e/4) + e/4) < e
-    3e/4<e = <WellDefined identLeft (transitive (+WellDefined reflexive (+WellDefined prE/4 reflexive)) (transitive groupIsAbelian (transitive (symmetric +Associative) (transitive (+WellDefined reflexive prE/4) prE/2)))) (orderRespectsAddition (halvePositive' prE/4 (halvePositive' prE/2 0<e)) ((e/4 + e/4) + e/4))
-    t : c' r<C (c +C injection e/4)
-    t = r<CWellDefinedRight _ _ _ (Ring.groupIsAbelian CRing {record { converges = CauchyCompletion.converges (injection e/4) }} {record { converges = CauchyCompletion.converges c }}) (cOrderMove' _ _ _ (<CRelaxR' c'-c<e/4))
-    u : (c' + e/2) r<C (c +C injection ((e/4 + e/4) + e/4))
-    u = r<CWellDefinedRight record { converges = CauchyCompletion.converges ((c +C injection e/4) +C (injection e/2))} _ _ {!!} (<CRelaxL' (<CWellDefined (GroupHom.groupHom' CInjectionGroupHom) (Equivalence.reflexive (Setoid.eq cauchyCompletionSetoid) {record { converges = CauchyCompletion.converges ((c +C injection e/4) +C injection e/2) }}) (cOrderRespectsAdditionLeft''' _ _ e/2 (<CRelaxL t))))
-    u' : ((c' + e/4) + e/4) r<C (c +C injection ((e/4 + e/4) + e/4))
-    u' = r<CWellDefinedLeft _ _ _ (transitive (+WellDefined reflexive (symmetric prE/4)) +Associative) u
-    v : (c +C injection ((e/4 + e/4) + e/4)) <Cr (cB + (((e/4 + e/4) + e/4) + e/8))
-    v with cOrderMove'' _ _ _ (<CRelaxR' c-cB<e/8)
-    ... | c<cB+e/8 = <CRelaxR' (<CWellDefined (Equivalence.reflexive (Setoid.eq cauchyCompletionSetoid) {record { converges = CauchyCompletion.converges (c +C injection ((e/4 + e/4) + e/4))}}) (Equivalence.transitive (Setoid.eq cauchyCompletionSetoid) {record { converges = CauchyCompletion.converges ((injection (cB + e/8)) +C (injection ((e/4 + e/4) + e/4))) }} {record { converges = CauchyCompletion.converges (injection ((cB + e/8) + ((e/4 + e/4) + e/4))) }} {record { converges = CauchyCompletion.converges (injection (cB + (((e/4 + e/4) + e/4) + e/8))) }} (GroupHom.groupHom' CInjectionGroupHom) (GroupHom.wellDefined CInjectionGroupHom (transitive (symmetric +Associative) (+WellDefined reflexive groupIsAbelian)))) (cOrderRespectsAdditionLeft''' _ _ ((e/4 + e/4) + e/4) (<CRelaxR c<cB+e/8)))
-    w : (m : ℕ) → (N<m : N <N m) → (c +C injection ((e/4 + e/4) + e/4)) <Cr ((index (CauchyCompletion.elts a) m) + (index (CauchyCompletion.elts c) m))
-    w = {!!}
-    --pr2      : (m₁ : ℕ) → N2 <N m₁ → (f + index (CauchyCompletion.elts c) m₁) < (cB + e/8)
-    req : (m : ℕ) → (N<m : N <N m) → ((c' + e/4) + e/4) < index (apply _+_ (CauchyCompletion.elts a) (CauchyCompletion.elts c)) m
-    req = {!!}
-    {-
-    ans : (m : ℕ) → (N<m : N <N m) → (c' + e/2) r<C (injection (index (CauchyCompletion.elts a) m) +C c)
-    ans m N<m = <CRelaxL' (<CTransitive (<CRelaxL u) (<CTransitive v (w m N<m)))
-    req : (m : ℕ) → (N<m : N <N m) → ((c' + e/4) + e/4) < index (apply _+_ (CauchyCompletion.elts a) (CauchyCompletion.elts c)) m
-    req m N<m with ans m N<m
-    ... | record { e = f ; 0<e = 0<f ; N = M ; pr = pr } with pr m {!!}
-    ... | t rewrite indexAndApply (CauchyCompletion.elts a) (CauchyCompletion.elts c) _+_ {m} | indexAndConst (CauchyCompletion.elts a) m = {!!}
-    -}
+  cOrderRespectsAdditionRightZero : (a : CauchyCompletion) → (0R r<C a) → (c : CauchyCompletion) → c <C (a +C c)
+  cOrderRespectsAdditionRightZero a record { e = e ; 0<e = 0<e ; N = N1 ; pr = pr } c with halve charNot2 e
+  ... | e/2 , prE/2 with approximateAbove c e/2 (halvePositive' prE/2 0<e)
+  ... | c+ , (c<c+ ,, c+<c+e/2) with approximateBelow (a +C c) e/2 (halvePositive' prE/2 0<e)
+  ... | α , (α<a+c ,, a+c<α+e/2) with totality c+ α
+  ... | inl (inl c+<α) = record { i = α ; a<i = <CRelaxR' (<CTransitive (<CRelaxR c<c+) (<CInherited c+<α)) ; i<b = α<a+c }
+  -- The remaining cases can't actually happen, but it's easier to go this way
+  ... | inr c+=α = record { i = α ; a<i = <CrWellDefinedRight c _ _ c+=α c<c+ ; i<b = α<a+c }
+  ... | inl (inr α<c+) with cOrderMove'' (a +C c) α e/2 (<CRelaxR' a+c<α+e/2)
+  ... | record { e = f ; 0<e = 0<f ; N = M ; property = pr2 } with CauchyCompletion.converges c e/2 (halvePositive' prE/2 0<e)
+  ... | N3 , pr4 = record { i = α ; a<i = record { e = f ; 0<e = 0<f ; N = u ; property = ans } ; i<b = α<a+c }
+    where
+      u : ℕ
+      u = succ ((N1 +N M) +N N3)
+      help : (m : ℕ) → u <N m → index (CauchyCompletion.elts c) m < (e/2 + index (CauchyCompletion.elts c) u)
+      help m size with pr4 {m} {u} (lessTransitive (le (N1 +N M) refl) size) (le (N1 +N M) refl)
+      ... | bl with totality 0G (index (CauchyCompletion.elts c) m + inverse (index (CauchyCompletion.elts c) u))
+      ... | inl (inl 0<t) = <WellDefined (transitive (symmetric +Associative) (transitive (+WellDefined reflexive invLeft) identRight)) reflexive (orderRespectsAddition bl (index (CauchyCompletion.elts c) u))
+      ... | inl (inr cm-cU<0) = <Transitive (<WellDefined (transitive (transitive (symmetric +Associative) (+WellDefined reflexive invLeft)) identRight) reflexive (orderRespectsAddition cm-cU<0 (index (CauchyCompletion.elts c) u))) (orderRespectsAddition (halvePositive' prE/2 0<e) (index (CauchyCompletion.elts c) u))
+      ... | inr (0=t) = <WellDefined (transitive (symmetric +Associative) (transitive (+WellDefined reflexive invLeft) identRight)) reflexive (orderRespectsAddition bl (index (CauchyCompletion.elts c) u))
+      ans : (m : ℕ) → u <N m → (f + index (CauchyCompletion.elts c) m) < α
+      ans m size = <Transitive (<WellDefined reflexive +Associative (<WellDefined groupIsAbelian groupIsAbelian (orderRespectsAddition (<Transitive (<WellDefined reflexive (transitive (+WellDefined (symmetric (transitive (+WellDefined (transitive identLeft (symmetric prE/2)) reflexive) (transitive (transitive (symmetric +Associative) (+WellDefined reflexive invRight)) identRight))) reflexive) (symmetric +Associative)) (help m size)) (<WellDefined reflexive (transitive groupIsAbelian (transitive (symmetric +Associative) (+WellDefined reflexive groupIsAbelian))) (orderRespectsAddition (pr u (le (M +N N3) (applyEquality succ (transitivity (additionNIsCommutative _ N1) (Semiring.+Associative ℕSemiring N1 M _))))) (inverse e/2 + index (CauchyCompletion.elts c) u)))) f))) (<WellDefined (transitive groupIsAbelian (transitive +Associative (+WellDefined groupIsAbelian (identityOfIndiscernablesRight _∼_ reflexive (indexAndApply (CauchyCompletion.elts a) (CauchyCompletion.elts c) _+_ {u}))))) (transitive (transitive (symmetric +Associative) (+WellDefined reflexive invRight)) identRight) (orderRespectsAddition (pr2 u (le (N1 +N N3) (applyEquality succ (transitivity (equalityCommutative (Semiring.+Associative ℕSemiring N1 _ _)) (transitivity (applyEquality (N1 +N_) (additionNIsCommutative N3 M)) (Semiring.+Associative ℕSemiring N1 _ _)))))) (inverse e/2)))
 
-cOrderRespectsAdditionLeft : (a : CauchyCompletion) (b : A) (c : CauchyCompletion) → (a <Cr b) → (a +C c) <C (injection b +C c)
-cOrderRespectsAdditionLeft a b c a<b = <CWellDefined {record { converges = CauchyCompletion.converges (a +C c) }}{record { converges = CauchyCompletion.converges (a +C c) }}{record { converges = CauchyCompletion.converges (((-C a) +C injection b) +C (a +C c)) }}{record { converges = CauchyCompletion.converges (injection b +C c) }} (Equivalence.reflexive (Setoid.eq cauchyCompletionSetoid) {record { converges = CauchyCompletion.converges (a +C c)}}) (lemma3 CGroup (λ {x} {y} → Ring.groupIsAbelian CRing {x} {y}) a (injection b) c) (cOrderRespectsAdditionRightZero ((-C a) +C injection b) (r<CWellDefinedLeft (inverse b + b) 0R ((-C a) +C injection b) invLeft (<CRelaxL' (<CWellDefined {record { converges = CauchyCompletion.converges (injection (inverse b) +C injection b) }}{record { converges = CauchyCompletion.converges (injection (inverse b + b)) }}{record { converges = CauchyCompletion.converges ((-C a) +C injection b) }}{record { converges = CauchyCompletion.converges ((-C a) +C injection b) }} (GroupHom.groupHom' CInjectionGroupHom) (Equivalence.reflexive (Setoid.eq cauchyCompletionSetoid) {record { converges = CauchyCompletion.converges ((-C a) +C injection b) }}) (cOrderRespectsAdditionLeft''' _ _ b (<CRelaxL (flip<CR a<b)))))) (a +C c))
+  cOrderRespectsAdditionLeft : (a : CauchyCompletion) (b : A) (c : CauchyCompletion) → (a <Cr b) → (a +C c) <C (injection b +C c)
+  cOrderRespectsAdditionLeft a b c a<b = <CWellDefined {record { converges = CauchyCompletion.converges (a +C c) }}{record { converges = CauchyCompletion.converges (a +C c) }}{record { converges = CauchyCompletion.converges (((-C a) +C injection b) +C (a +C c)) }}{record { converges = CauchyCompletion.converges (injection b +C c) }} (Equivalence.reflexive (Setoid.eq cauchyCompletionSetoid) {record { converges = CauchyCompletion.converges (a +C c)}}) (lemma3 CGroup (λ {x} {y} → Ring.groupIsAbelian CRing {x} {y}) a (injection b) c) (cOrderRespectsAdditionRightZero ((-C a) +C injection b) (r<CWellDefinedLeft (inverse b + b) 0R ((-C a) +C injection b) invLeft (<CRelaxL' (<CWellDefined {record { converges = CauchyCompletion.converges (injection (inverse b) +C injection b) }}{record { converges = CauchyCompletion.converges (injection (inverse b + b)) }}{record { converges = CauchyCompletion.converges ((-C a) +C injection b) }}{record { converges = CauchyCompletion.converges ((-C a) +C injection b) }} (GroupHom.groupHom' CInjectionGroupHom) (Equivalence.reflexive (Setoid.eq cauchyCompletionSetoid) {record { converges = CauchyCompletion.converges ((-C a) +C injection b) }}) (cOrderRespectsAdditionLeft''' _ _ b (<CRelaxL (flip<CR a<b)))))) (a +C c))
 
-private
   lemma2 : (a b : CauchyCompletion) → Setoid._∼_ cauchyCompletionSetoid (Group.inverse CGroup ((-C a) +C (-C b))) (a +C b)
   lemma2 a b = tr {record { converges = CauchyCompletion.converges (-C ((-C a) +C (-C b))) }} {record { converges = CauchyCompletion.converges ((-C (-C b)) +C (-C (-C a))) }} {record { converges = CauchyCompletion.converges (a +C b) }} (invContravariant CGroup {record { converges = CauchyCompletion.converges (-C a) }} {record { converges = CauchyCompletion.converges (-C b) }}) (tr {record { converges = CauchyCompletion.converges ((-C (-C b)) +C (-C (-C a))) }} {record { converges = CauchyCompletion.converges (b +C a) }} {record { converges = CauchyCompletion.converges (a +C b) }} (Group.+WellDefined CGroup {record { converges = CauchyCompletion.converges (-C (-C b)) }} {record { converges = CauchyCompletion.converges (-C (-C a)) }} {record { converges = CauchyCompletion.converges b }} {record { converges = CauchyCompletion.converges a }} (invTwice CGroup b) (invTwice CGroup a)) (Ring.groupIsAbelian CRing {record { converges = CauchyCompletion.converges b }} {record { converges = CauchyCompletion.converges a }}))
     where
       open Setoid cauchyCompletionSetoid
       open Equivalence (Setoid.eq cauchyCompletionSetoid) renaming (transitive to tr)
 
-cOrderRespectsAdditionRight : (a : A) (b : CauchyCompletion) (c : CauchyCompletion) → (a r<C b) → (injection a +C c) <C (b +C c)
-cOrderRespectsAdditionRight a b c a<b = <CWellDefined (Equivalence.transitive (Setoid.eq cauchyCompletionSetoid) {record { converges = CauchyCompletion.converges (Group.inverse CGroup (injection (inverse a) +C (-C c))) }} {record { converges = CauchyCompletion.converges (Group.inverse CGroup ((-C injection a) +C (-C c))) }} {record { converges = CauchyCompletion.converges (injection a +C c) }} (inverseWellDefined CGroup {record { converges = CauchyCompletion.converges (injection (inverse a) +C (-C c)) }} {record { converges = CauchyCompletion.converges ((-C (injection a)) +C (-C c)) }} (Group.+WellDefined CGroup {record { converges = CauchyCompletion.converges (injection (inverse a)) }} {record { converges = CauchyCompletion.converges (-C c) }} {record { converges = CauchyCompletion.converges (-C (injection a)) }} {record { converges = CauchyCompletion.converges (-C c) }} homRespectsInverse (Equivalence.reflexive (Setoid.eq cauchyCompletionSetoid) {record { converges = CauchyCompletion.converges (-C c) }}))) (lemma2 (injection a) c)) (lemma2 b c) (flip<C (cOrderRespectsAdditionLeft _ _ (Group.inverse CGroup c) (flipR<C a<b)))
+  cOrderRespectsAdditionRight : (a : A) (b : CauchyCompletion) (c : CauchyCompletion) → (a r<C b) → (injection a +C c) <C (b +C c)
+  cOrderRespectsAdditionRight a b c a<b = <CWellDefined (Equivalence.transitive (Setoid.eq cauchyCompletionSetoid) {record { converges = CauchyCompletion.converges (Group.inverse CGroup (injection (inverse a) +C (-C c))) }} {record { converges = CauchyCompletion.converges (Group.inverse CGroup ((-C injection a) +C (-C c))) }} {record { converges = CauchyCompletion.converges (injection a +C c) }} (inverseWellDefined CGroup {record { converges = CauchyCompletion.converges (injection (inverse a) +C (-C c)) }} {record { converges = CauchyCompletion.converges ((-C (injection a)) +C (-C c)) }} (Group.+WellDefined CGroup {record { converges = CauchyCompletion.converges (injection (inverse a)) }} {record { converges = CauchyCompletion.converges (-C c) }} {record { converges = CauchyCompletion.converges (-C (injection a)) }} {record { converges = CauchyCompletion.converges (-C c) }} homRespectsInverse (Equivalence.reflexive (Setoid.eq cauchyCompletionSetoid) {record { converges = CauchyCompletion.converges (-C c) }}))) (lemma2 (injection a) c)) (lemma2 b c) (flip<C (cOrderRespectsAdditionLeft _ _ (Group.inverse CGroup c) (flipR<C a<b)))
 
-cOrderRespectsAddition : (a b : CauchyCompletion) → (a <C b) → (c : CauchyCompletion) → (a +C c) <C (b +C c)
-cOrderRespectsAddition a b record { i = i ; a<i = a<i ; i<b = i<b } c = SetoidPartialOrder.<Transitive <COrder (cOrderRespectsAdditionLeft a i c a<i) (cOrderRespectsAdditionRight i b c i<b)
+  cOrderRespectsAddition : (a b : CauchyCompletion) → (a <C b) → (c : CauchyCompletion) → (a +C c) <C (b +C c)
+  cOrderRespectsAddition a b record { i = i ; a<i = a<i ; i<b = i<b } c = SetoidPartialOrder.<Transitive <COrder (cOrderRespectsAdditionLeft a i c a<i) (cOrderRespectsAdditionRight i b c i<b)
 
 CpOrderedRing : PartiallyOrderedRing CRing <COrder
 PartiallyOrderedRing.orderRespectsAddition CpOrderedRing {a} {b} = cOrderRespectsAddition a b