diff --git a/Everything/Safe.agda b/Everything/Safe.agda
index de1b0a1..cb3efb0 100644
--- a/Everything/Safe.agda
+++ b/Everything/Safe.agda
@@ -56,6 +56,6 @@ open import Semirings.Definition
 open import Semirings.Solver
 
 open import Fields.CauchyCompletion.Group
-open import Fields.CauchyCompletion.Comparison
+open import Fields.CauchyCompletion.Approximation
 
 module Everything.Safe where
diff --git a/Fields/CauchyCompletion/Approximation.agda b/Fields/CauchyCompletion/Approximation.agda
index d91c555..bdabaa3 100644
--- a/Fields/CauchyCompletion/Approximation.agda
+++ b/Fields/CauchyCompletion/Approximation.agda
@@ -1,6 +1,7 @@
 {-# OPTIONS --safe --warning=error --without-K --guardedness #-}
 
 open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
+open import Orders
 open import Setoids.Setoids
 open import Rings.Definition
 open import Rings.Lemmas
@@ -14,6 +15,8 @@ open import Setoids.Orders
 open import Functions
 open import LogicalFormulae
 open import Numbers.Naturals.Naturals
+open import Numbers.Naturals.Order
+open import Semirings.Definition
 
 module Fields.CauchyCompletion.Approximation {m n o : _} {A : Set m} {S : Setoid {m} {n} A} {_+_ : A → A → A} {_*_ : A → A → A} {_<_ : Rel {m} {o} A} {pOrder : SetoidPartialOrder S _<_} {tOrder : SetoidTotalOrder {_<_ = _<_} pOrder} {R : Ring S _+_ _*_} (order : OrderedRing R tOrder) (F : Field R) (charNot2 : Setoid._∼_ S ((Ring.1R R) + (Ring.1R R)) (Ring.0R R) → False) where
 
@@ -26,10 +29,174 @@ open Ring R
 open Group additiveGroup
 open Field F
 
+open import Fields.Lemmas F
+open import Fields.Orders.Lemmas {F = F} record { oRing = order }
 open import Rings.Orders.Lemmas(order)
 open import Fields.CauchyCompletion.Definition order F
 open import Fields.CauchyCompletion.Addition order F charNot2
 open import Fields.CauchyCompletion.Setoid order F charNot2
+open import Fields.CauchyCompletion.Comparison order F charNot2
 
-approximate : (a : CauchyCompletion) → (ε : A) → Sg A (λ b → a +C (-C (injection b)) < ε)
-approximate a ε = ?
+chain : {a b : A} (c : CauchyCompletion) → (a r<C c) → (c <Cr b) → a < b
+chain {a} {b} c (betweenAC , (0<betweenAC ,, (Nac , prAC))) (betweenCB , (0<betweenCB ,, (Nb , prBC))) = SetoidPartialOrder.transitive pOrder (SetoidPartialOrder.transitive pOrder (<WellDefined identLeft (Equivalence.reflexive eq) (orderRespectsAddition 0<betweenAC a)) (<WellDefined groupIsAbelian (Equivalence.reflexive eq) (SetoidPartialOrder.transitive pOrder (prAC (succ Nac +N Nb) (le Nb (applyEquality succ (Semiring.commutative ℕSemiring Nb Nac)))) (<WellDefined identLeft (Equivalence.reflexive eq) (orderRespectsAddition 0<betweenCB (index (Sequence.tail (CauchyCompletion.elts c)) (Nac +N Nb))))))) (prBC (succ Nac +N Nb) (le Nac refl))
+
+approxLemma : (a : CauchyCompletion) (e e/2 : A) → (0G < e) → (e/2 + e/2 ∼ e) → (m N : ℕ) → abs ((index (CauchyCompletion.elts a) m) + inverse (index (CauchyCompletion.elts a) N)) < e/2 → (e/2 + index (CauchyCompletion.elts a) m) < (index (CauchyCompletion.elts a) N + e)
+approxLemma a e e/2 0<e prE/2 m N ans with SetoidTotalOrder.totality tOrder 0R ((index (CauchyCompletion.elts a) m) + inverse (index (CauchyCompletion.elts a) N))
+approxLemma a e e/2 0<e prE/2 m N ans | inl (inl x) with <WellDefined (Equivalence.transitive eq (Equivalence.transitive eq (Equivalence.symmetric eq +Associative) (+WellDefined (Equivalence.reflexive eq) (invLeft))) identRight) groupIsAbelian (orderRespectsAddition ans (index (CauchyCompletion.elts a) N))
+... | bl = <WellDefined groupIsAbelian (Equivalence.transitive eq (Equivalence.symmetric eq +Associative) (+WellDefined (Equivalence.reflexive eq) prE/2)) (orderRespectsAddition bl e/2)
+approxLemma a e e/2 0<e prE/2 m N ans | inl (inr x) with <WellDefined (Equivalence.transitive eq (Equivalence.transitive eq (Equivalence.symmetric eq +Associative) (+WellDefined (Equivalence.reflexive eq) (invLeft))) identRight) (identLeft) (orderRespectsAddition x (index (CauchyCompletion.elts a) N))
+... | bl = <WellDefined groupIsAbelian (Equivalence.reflexive eq) (ringAddInequalities bl (halfLess e/2 e 0<e prE/2))
+approxLemma a e e/2 0<e prE/2 m N ans | inr x with transferToRight additiveGroup (Equivalence.symmetric eq x)
+... | bl = <WellDefined (+WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq bl)) groupIsAbelian (orderRespectsAddition (halfLess e/2 e 0<e prE/2) (index (CauchyCompletion.elts a) N))
+
+approximateAboveCrude : (0R ∼ 1R → False) → (a : CauchyCompletion) → Sg A (λ b → (a <Cr b))
+approximateAboveCrude 0!=1 a with CauchyCompletion.converges a 1R (0<1 0!=1)
+... | N , conv = ((((index (CauchyCompletion.elts a) (succ N)) + 1R) + 1R) + 1R) , (1R , (0<1 0!=1 ,, (N , ans)))
+  where
+    ans : (m : ℕ) → (N <N m) → (1R + index (CauchyCompletion.elts a) m) < (((index (CauchyCompletion.elts a) (succ N) + 1R) + 1R) + 1R)
+    ans m N<m with conv {m} {succ N} N<m (le 0 refl)
+    ... | bl with totality 0G (index (CauchyCompletion.elts a) m + inverse (index (CauchyCompletion.elts a) (succ N)))
+    ans m N<m | bl | inl (inl 0<am-aN) with <WellDefined (Equivalence.transitive eq (Equivalence.transitive eq (Equivalence.symmetric eq +Associative) (+WellDefined (Equivalence.reflexive eq) (invLeft))) identRight) (Equivalence.reflexive eq) (orderRespectsAddition bl (index (CauchyCompletion.elts a) (succ N)))
+    ... | am<1+an = <WellDefined (Equivalence.transitive eq (+WellDefined (Equivalence.reflexive eq) identLeft) groupIsAbelian) (Equivalence.transitive eq (+WellDefined groupIsAbelian (Equivalence.reflexive eq)) +Associative) (ringAddInequalities am<1+an (orderRespectsAddition (0<1 0!=1) 1R))
+    ans m N<m | bl | inl (inr am-aN<0) with <WellDefined (Equivalence.transitive eq (Equivalence.transitive eq (Equivalence.symmetric eq +Associative) (+WellDefined (Equivalence.reflexive eq) invLeft)) identRight) identLeft (orderRespectsAddition am-aN<0 (index (CauchyCompletion.elts a) (succ N)))
+    ... | am<aN = <WellDefined groupIsAbelian (Equivalence.reflexive eq) (orderRespectsAddition (SetoidPartialOrder.transitive pOrder am<aN (<WellDefined (Equivalence.reflexive eq) (+Associative) (<WellDefined identLeft groupIsAbelian (orderRespectsAddition (<WellDefined identLeft (Equivalence.reflexive eq) (ringAddInequalities (0<1 0!=1) (0<1 0!=1))) (index (CauchyCompletion.elts a) (succ N)))))) 1R)
+    ans m N<m | bl | inr 0=am-aN = <WellDefined (Equivalence.transitive eq (+WellDefined identLeft (Equivalence.reflexive eq)) identLeft) (Equivalence.transitive eq groupIsAbelian (Equivalence.transitive eq (+WellDefined (Equivalence.transitive eq groupIsAbelian (+WellDefined (transferToRight additiveGroup (Equivalence.symmetric eq 0=am-aN)) (Equivalence.reflexive eq))) (Equivalence.reflexive eq)) +Associative)) (orderRespectsAddition (ringAddInequalities (0<1 0!=1) (0<1 0!=1)) (1R + (index (CauchyCompletion.elts a) m)))
+
+rationalApproximatelyAbove : (a : CauchyCompletion) → (e : A) → (0G < e) → A
+rationalApproximatelyAbove a e 0<e with halve charNot2 e
+... | e/2 , prE/2 with halvePositive e/2 (<WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq prE/2) 0<e)
+... | 0<e/2 with halve charNot2 e/2
+... | e/4 , prE/4 with halvePositive e/4 (<WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq prE/4) 0<e/2)
+... | 0<e/4 with CauchyCompletion.converges a e/4 0<e/4
+... | N , cauchyBeyondN = index (CauchyCompletion.elts a) (succ N) + e/2
+
+rationalApproximatelyAboveIsAbove : (a : CauchyCompletion) (e : A) → (0<e : 0G < e) → a <Cr (rationalApproximatelyAbove a e 0<e)
+rationalApproximatelyAboveIsAbove a e 0<e with halve charNot2 e
+... | e/2 , prE/2 with halvePositive e/2 (<WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq prE/2) 0<e)
+... | 0<e/2 with halve charNot2 e/2
+... | e/4 , prE/4 with halvePositive e/4 (<WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq prE/4) 0<e/2)
+... | 0<e/4 with CauchyCompletion.converges a e/4 0<e/4
+... | N , cauchyBeyondN with halve charNot2 e/4
+... | e/8 , prE/8 with halvePositive e/8 (<WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq prE/8) 0<e/4)
+... | 0<e/8 with CauchyCompletion.converges a e/8 0<e/8
+... | N2 , cauchyBeyondN2 = e/8 , (0<e/8 ,, ((N +N N2) , ans2))
+  where
+    ans2 : (m : ℕ) → N +N N2 <N m → (e/8 + index (CauchyCompletion.elts a) m) < (index (CauchyCompletion.elts a) (succ N) + e/2) -- TODO not sure this is actually true
+    ans2 m <m with cauchyBeyondN {m} {succ N} (inequalityShrinkLeft <m) (le 0 refl)
+    ... | absam-aN<e/4 with totality 0R ((index (CauchyCompletion.elts a) m) + inverse (index (CauchyCompletion.elts a) (succ N)))
+    ans2 m <m | am-aN<e/4 | inl (inl 0<am-aN) = SetoidPartialOrder.transitive pOrder (<WellDefined groupIsAbelian (Equivalence.transitive eq groupIsAbelian  +Associative) (orderRespectsAddition (<WellDefined (Equivalence.transitive eq (Equivalence.transitive eq (Equivalence.symmetric eq +Associative) (+WellDefined (Equivalence.reflexive eq) invLeft)) identRight) (Equivalence.reflexive eq) (orderRespectsAddition am-aN<e/4 (index (CauchyCompletion.elts a) (succ N)))) e/8)) (<WellDefined (Equivalence.reflexive eq) groupIsAbelian (orderRespectsAddition (<WellDefined (Equivalence.reflexive eq) prE/4 (orderRespectsAddition (halfLess e/8 e/4 0<e/4 prE/8) e/4)) (index (CauchyCompletion.elts a) (succ N))))
+    ans2 m <m | -[am-aN]<e/4 | inl (inr am-aN<0) with <WellDefined (Equivalence.transitive eq +Associative (Equivalence.transitive eq (+WellDefined invLeft (Equivalence.reflexive eq)) identLeft)) (Equivalence.reflexive eq) (orderRespectsAddition (<WellDefined (Equivalence.reflexive eq) (invTwice additiveGroup _) (ringSwapNegatives' -[am-aN]<e/4)) (e/4 + e/8))
+    ... | e/8<am-aN+e/4+e/8 = SetoidPartialOrder.transitive pOrder (orderRespectsAddition e/8<am-aN+e/4+e/8 (index (CauchyCompletion.elts a) m)) (<WellDefined (Equivalence.reflexive eq) groupIsAbelian (ringAddInequalities (<WellDefined (Equivalence.reflexive eq) identLeft (ringAddInequalities am-aN<0 (<WellDefined groupIsAbelian prE/4 (orderRespectsAddition (halfLess e/8 e/4 0<e/4 prE/8) e/4)))) am<aN))
+      where
+        am<aN : (index (CauchyCompletion.elts a) m) < (index (CauchyCompletion.elts a) (succ N))
+        am<aN = <WellDefined (Equivalence.transitive eq (Equivalence.transitive eq (Equivalence.symmetric eq +Associative) (+WellDefined (Equivalence.reflexive eq) groupIsAbelian)) (Equivalence.transitive eq (+WellDefined (Equivalence.reflexive eq) invRight) identRight)) identLeft (orderRespectsAddition am-aN<0 (index (CauchyCompletion.elts a) (succ N)))
+    ans2 m <m | absam-aN<e/4 | inr 0=am-aN = <WellDefined (Equivalence.reflexive eq) (Equivalence.transitive eq groupIsAbelian (+WellDefined (transferToRight additiveGroup (Equivalence.symmetric eq 0=am-aN)) (Equivalence.reflexive eq))) (orderRespectsAddition {b = e/2} (SetoidPartialOrder.transitive pOrder (halfLess e/8 e/4 0<e/4 prE/8) (halfLess e/4 e/2 0<e/2 prE/4)) (index (CauchyCompletion.elts a) m))
+
+rationalApproximatelyAboveIsNear : (a : CauchyCompletion) (e : A) → (0<e : 0G < e) → (injection (rationalApproximatelyAbove a e 0<e) +C (-C a)) <C (injection e)
+rationalApproximatelyAboveIsNear a e 0<e with halve charNot2 e
+... | e/2 , prE/2 with halvePositive e/2 (<WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq prE/2) 0<e)
+... | 0<e/2 with halve charNot2 e/2
+... | e/4 , prE/4 with halvePositive e/4 (<WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq prE/4) 0<e/2)
+... | 0<e/4 with CauchyCompletion.converges a e/4 0<e/4
+... | N , cauchyBeyondN with halve charNot2 e/4
+... | e/8 , prE/8 with halvePositive e/8 (<WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq prE/8) 0<e/4)
+... | 0<e/8 with CauchyCompletion.converges a e/8 0<e/8
+... | N8 , cauchyBeyondN8 with halve charNot2 e/8
+... | e/16 , prE/16 with halvePositive e/16 (<WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq prE/16) 0<e/8)
+... | 0<e/16 = ((e/2 + e/4) + e/8) , ((e/8 , (0<e/8 ,, ((N +N N8) , ans))) ,, (e/16 , (0<e/16 ,, (0 , t'))))
+  where
+    t' : (m : ℕ) → (0 <N m) → (((e/2 + e/4) + e/8) + e/16) < index (constSequence e) m
+    t' m 0<m rewrite indexAndConst e m = <WellDefined (Equivalence.reflexive eq) prE/2 (<WellDefined (Equivalence.reflexive eq) (+WellDefined (Equivalence.reflexive eq) prE/4) (<WellDefined +Associative (Equivalence.symmetric eq +Associative) (<WellDefined groupIsAbelian groupIsAbelian (orderRespectsAddition (<WellDefined (Equivalence.reflexive eq) prE/8 (<WellDefined groupIsAbelian groupIsAbelian (orderRespectsAddition (halfLess e/16 e/8 0<e/8 prE/16) e/8))) (e/2 + e/4)))))
+    ans : (m : ℕ) → (N +N N8) <N m → (e/8 + index (apply _+_ (constSequence (index (CauchyCompletion.elts a) (succ N) + e/2)) (map inverse (CauchyCompletion.elts a))) m) < ((e/2 + e/4) + e/8)
+    ans m N<m rewrite indexAndApply (constSequence (index (CauchyCompletion.elts a) (succ N) + e/2)) (map inverse (CauchyCompletion.elts a)) _+_ {m} | indexAndConst (index (CauchyCompletion.elts a) (succ N) + e/2) m | equalityCommutative (mapAndIndex (CauchyCompletion.elts a) inverse m) = <WellDefined groupIsAbelian (+WellDefined groupIsAbelian (Equivalence.reflexive eq)) (orderRespectsAddition (<WellDefined (Equivalence.transitive eq groupIsAbelian (Equivalence.reflexive eq)) (Equivalence.reflexive eq) q) e/8)
+      where
+        am = index (CauchyCompletion.elts a) m
+        aN = index (CauchyCompletion.elts a) (succ N)
+        t : abs (am + inverse aN) < e/4
+        t = cauchyBeyondN {m} {succ N} (inequalityShrinkLeft N<m) (le 0 refl)
+        r : ((inverse am) + aN) < e/4
+        r with t
+        ... | f with totality 0G (am + inverse aN)
+        r | am-aN<e/4 | inl (inl 0<am-aN) = SetoidPartialOrder.transitive pOrder (<WellDefined (Equivalence.transitive eq (invContravariant additiveGroup) (Equivalence.transitive eq groupIsAbelian (+WellDefined (Equivalence.reflexive eq) (invTwice additiveGroup _)))) (Equivalence.reflexive eq) (lemm2' _ 0<am-aN)) 0<e/4
+        r | f | inl (inr x) = <WellDefined (Equivalence.transitive eq (invContravariant additiveGroup) (Equivalence.transitive eq groupIsAbelian (+WellDefined (Equivalence.reflexive eq) (invTwice additiveGroup _)))) (Equivalence.reflexive eq) f
+        r | am-aN<e/4 | inr 0=am-aN = <WellDefined (Equivalence.transitive eq (Equivalence.symmetric eq 0=am-aN) (Equivalence.transitive eq (Equivalence.transitive eq (Equivalence.transitive eq (Equivalence.transitive eq (Equivalence.symmetric eq (invIdentity additiveGroup)) (inverseWellDefined additiveGroup 0=am-aN)) (inverseWellDefined additiveGroup groupIsAbelian)) (invContravariant additiveGroup)) (+WellDefined (Equivalence.reflexive eq) (invTwice additiveGroup _)))) (Equivalence.reflexive eq) am-aN<e/4
+        q : ((inverse (index (CauchyCompletion.elts a) m)) + (index (CauchyCompletion.elts a) (succ N) + e/2)) < (e/4 + e/2)
+        q = <WellDefined (Equivalence.symmetric eq +Associative) (Equivalence.reflexive eq) (orderRespectsAddition r e/2)
+
+approximateAbove : (a : CauchyCompletion) → (ε : A) → (0G < ε) → Sg A (λ b → (a <Cr b) && (injection b +C (-C a)) <C (injection ε))
+approximateAbove a e 0<e = rationalApproximatelyAbove a e 0<e , (rationalApproximatelyAboveIsAbove a e 0<e ,, rationalApproximatelyAboveIsNear a e 0<e)
+
+approximateBelow : (a : CauchyCompletion) → (ε : A) → (0G < ε) → Sg A (λ b → (b r<C a) && (a +C (-C injection b)) <C (injection ε))
+approximateBelow a e 0<e with approximateAbove (-C a) e 0<e
+... | x , ((deltaXAnd-A , (0<deltaXA ,, (NdeltaXA , prDeltaXA))) ,, (rationalNear , ((bound , (0<bound ,, (N , prBound))) ,, (bound2 , (0<bound2 ,, (N2 , prBound2)))))) = inverse x , ((deltaXAnd-A , (0<deltaXA ,, (NdeltaXA , λ m N<m → <WellDefined (Equivalence.transitive eq groupIsAbelian (Equivalence.transitive eq (Equivalence.symmetric eq +Associative) (+WellDefined (Equivalence.reflexive eq) (Equivalence.transitive eq groupIsAbelian (Equivalence.transitive eq (Equivalence.symmetric eq +Associative) (Equivalence.transitive eq (+WellDefined (Equivalence.reflexive eq) (cancel {m} (CauchyCompletion.elts a))) identRight)))))) (Equivalence.transitive eq +Associative (Equivalence.transitive eq (+WellDefined invRight (Equivalence.reflexive eq)) identLeft)) (orderRespectsAddition (prDeltaXA m N<m) (inverse x + (index (CauchyCompletion.elts a) m)))))) ,, (rationalNear , ((bound , (0<bound ,, (N , pr1))) ,, (bound2 , (0<bound2 ,, (N2 , prBound2))))))
+  where
+    cancel : {m : ℕ} (a : Sequence A) → (index (map inverse a) m) + (index a m) ∼ 0G
+    cancel {m} a rewrite equalityCommutative (mapAndIndex a inverse m) = invLeft
+    pr1 : (m : ℕ) → (N <N m) → (bound + index (apply _+_ (CauchyCompletion.elts a) (map inverse (constSequence (inverse x)))) m) < rationalNear
+    pr1 m N<m with prBound m N<m
+    ... | bl rewrite indexAndApply (CauchyCompletion.elts a) (map inverse (constSequence (inverse x))) _+_ {m} | equalityCommutative (mapAndIndex (constSequence (inverse x)) inverse m) | indexAndConst x m | indexAndApply (constSequence x) (map inverse (map inverse (CauchyCompletion.elts a))) _+_ {m} | indexAndConst x m | equalityCommutative (mapAndIndex (map inverse (CauchyCompletion.elts a)) inverse m) | equalityCommutative (mapAndIndex (CauchyCompletion.elts a) inverse m) | indexAndConst (inverse x) m = <WellDefined (+WellDefined (Equivalence.reflexive eq) (Equivalence.transitive eq groupIsAbelian (+WellDefined (invTwice additiveGroup _) (Equivalence.symmetric eq (invTwice additiveGroup _))))) (Equivalence.reflexive eq) bl
+
+boundModulus' : (0R < 1R) → (a : CauchyCompletion) → Sg A (λ b → Sg ℕ (λ N → (m : ℕ) → (N <N m) → (abs (index (CauchyCompletion.elts a) m)) < b))
+boundModulus' 0!=1 a with approximateBelow a 1R 0!=1
+... | below , (below<a ,, a-below<e) with approximateAbove a 1R 0!=1
+... | above , (a<above ,, above-a<e) with SetoidTotalOrder.totality tOrder 0R below
+boundModulus' 0!=1 a | below , (below<a ,, a-below<e) | above , (a<above ,, above-a<e) | inl (inl 0<below) with SetoidTotalOrder.totality tOrder 0R above
+boundModulus' 0!=1 a | below , ((belowBound , (0<belowBound ,, (Nbelow , prBelow))) ,, a-below<e) | above , ((bound , (0<bound ,, (N , ans))) ,, above-a<e) | inl (inl 0<below) | inl (inl 0<above) = above , ((N +N Nbelow) , λ m N<m → SetoidPartialOrder.transitive pOrder (res m N<m) (ans m (inequalityShrinkLeft N<m)))
+  where
+    res : (m : ℕ) → ((N +N Nbelow) <N m) → (abs (index (CauchyCompletion.elts a) m)) < (bound + index (CauchyCompletion.elts a) m)
+    res m N<m with SetoidTotalOrder.totality tOrder 0R (index (CauchyCompletion.elts a) m)
+    res m N<m | inl (inl _) = <WellDefined identLeft (Equivalence.reflexive eq) (orderRespectsAddition 0<bound (index (CauchyCompletion.elts a) m))
+    res m N<m | inl (inr am<0) = exFalso (irreflexive (SetoidPartialOrder.transitive pOrder 0<below (SetoidPartialOrder.transitive pOrder (SetoidPartialOrder.transitive pOrder (<WellDefined identLeft groupIsAbelian (orderRespectsAddition 0<belowBound below)) (prBelow m (inequalityShrinkRight N<m))) am<0)))
+    res m N<m | inr 0=am = <WellDefined 0=am (Equivalence.transitive eq (Equivalence.symmetric eq identRight) (+WellDefined (Equivalence.reflexive eq) 0=am)) 0<bound
+boundModulus' 0!=1 a | below , (below<a ,, a-below<e) | above , (a<above ,, above-a<e) | inl (inl 0<below) | inl (inr above<0) = exFalso (irreflexive (SetoidPartialOrder.transitive pOrder 0<below (SetoidPartialOrder.transitive pOrder (chain a below<a a<above) above<0)))
+boundModulus' 0!=1 a | below , (below<a ,, a-below<e) | above , (a<above ,, above-a<e) | inl (inl 0<below) | inr 0=above = exFalso (irreflexive (SetoidPartialOrder.transitive pOrder 0<below (<WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq 0=above) (chain a below<a a<above))))
+boundModulus' 0!=1 a | below , (below<a ,, a-below<e) | above , (a<above ,, above-a<e) | inl (inr below<0) with SetoidTotalOrder.totality tOrder 0R above
+boundModulus' 0!=1 a | below , (below<a ,, a-below<e) | above , (a<above ,, above-a<e) | inl (inr below<0) | inl (inl 0<above) with SetoidTotalOrder.totality tOrder (inverse below) above
+boundModulus' 0!=1 a | below , ((boundBelow , (0<boundBelow ,, (N , prBoundBelow))) ,, a-below<e) | above , ((boundAbove , (0<boundAbove ,, (Nabove , prBoundAbove))) ,, above-a<e) | inl (inr below<0) | inl (inl 0<above) | inl (inl -bel<ab) = above , ((N +N Nabove) , ans)
+  where
+    ans : (m : ℕ) → (N +N Nabove <N m) → abs (index (CauchyCompletion.elts a) m) < above
+    ans m N<m with SetoidTotalOrder.totality tOrder 0G (index (CauchyCompletion.elts a) m)
+    ans m N<m | inl (inl 0<am) = SetoidPartialOrder.transitive pOrder (<WellDefined identLeft (Equivalence.reflexive eq) (orderRespectsAddition 0<boundAbove (index (CauchyCompletion.elts a) m))) (prBoundAbove m (inequalityShrinkRight N<m))
+    ans m N<m | inl (inr am<0) = SetoidPartialOrder.transitive pOrder (ringSwapNegatives' (prBoundBelow m (inequalityShrinkLeft N<m))) (SetoidPartialOrder.transitive pOrder (ringSwapNegatives' (<WellDefined identLeft groupIsAbelian (orderRespectsAddition 0<boundBelow below))) -bel<ab)
+    ans m N<m | inr 0=am = <WellDefined 0=am (Equivalence.reflexive eq) 0<above
+boundModulus' 0!=1 a | below , ((boundBelow , (0<boundBelow ,, (N , prBoundBelow))) ,, a-below<e) | above , ((boundAbove , (0<boundAbove ,, (Nabove , prBoundAbove))) ,, above-a<e) | inl (inr below<0) | inl (inl 0<above) | inl (inr ab<-bel) = inverse below , ((N +N Nabove) , ans)
+  where
+    ans : (m : ℕ) → (N +N Nabove <N m) → abs (index (CauchyCompletion.elts a) m) < (inverse below)
+    ans m N<m with SetoidTotalOrder.totality tOrder 0G (index (CauchyCompletion.elts a) m)
+    ans m N<m | inl (inl 0<am) = SetoidPartialOrder.transitive pOrder (SetoidPartialOrder.transitive pOrder (<WellDefined identLeft (Equivalence.reflexive eq) (orderRespectsAddition 0<boundAbove (index (CauchyCompletion.elts a) m))) (prBoundAbove m (inequalityShrinkRight N<m))) ab<-bel
+    ans m N<m | inl (inr am<0) = ringSwapNegatives' (SetoidPartialOrder.transitive pOrder (<WellDefined identLeft groupIsAbelian (orderRespectsAddition 0<boundBelow below)) (prBoundBelow m (inequalityShrinkLeft N<m)))
+    ans m N<m | inr 0=am = <WellDefined 0=am (Equivalence.reflexive eq) (lemm2 below below<0)
+boundModulus' 0!=1 a | below , ((boundBelow , (0<boundBelow ,, (N , prBoundBelow))) ,, a-below<e) | above , ((boundAbove , (0<boundAbove ,, (Nabove , prBoundAbove))) ,, above-a<e) | inl (inr below<0) | inl (inl 0<above) | inr -bel=ab = above , ((N +N Nabove) , ans)
+  where
+    ans : (m : ℕ) → (N +N Nabove <N m) → abs (index (CauchyCompletion.elts a) m) < above
+    ans m N<m with SetoidTotalOrder.totality tOrder 0G (index (CauchyCompletion.elts a) m)
+    ans m N<m | inl (inl 0<am) = SetoidPartialOrder.transitive pOrder (<WellDefined identLeft (Equivalence.reflexive eq) (orderRespectsAddition 0<boundAbove (index (CauchyCompletion.elts a) m))) (prBoundAbove m (inequalityShrinkRight N<m))
+    ans m N<m | inl (inr am<0) = <WellDefined (Equivalence.reflexive eq) (-bel=ab) (ringSwapNegatives' (SetoidPartialOrder.transitive pOrder (<WellDefined identLeft groupIsAbelian (orderRespectsAddition 0<boundBelow below)) (prBoundBelow m (inequalityShrinkLeft N<m))))
+    ans m N<m | inr 0=am = <WellDefined 0=am (Equivalence.reflexive eq) 0<above
+boundModulus' 0!=1 a | below , ((boundBelow , (0<boundBelow ,, (N , prBoundBelow))) ,, a-below<e) | above , ((boundAbove , (0<boundAbove ,, (Nabove , prBoundAbove))) ,, above-a<e) | inl (inr below<0) | inl (inr above<0) = inverse below , ((N +N Nabove) , ans)
+  where
+    ans : (m : ℕ) → ((N +N Nabove) <N m) → abs (index (CauchyCompletion.elts a) m) < inverse below
+    ans m N<m with SetoidTotalOrder.totality tOrder 0R (index (CauchyCompletion.elts a) m)
+    ans m N<m | inl (inl 0<am) = exFalso (irreflexive {0G} (SetoidPartialOrder.transitive pOrder 0<am (SetoidPartialOrder.transitive pOrder (SetoidPartialOrder.transitive pOrder (<WellDefined identLeft (Equivalence.reflexive eq) (orderRespectsAddition 0<boundAbove (index (CauchyCompletion.elts a) m))) (prBoundAbove m (inequalityShrinkRight N<m))) above<0)))
+    ans m N<m | inl (inr am<0) = ringSwapNegatives' (SetoidPartialOrder.transitive pOrder (<WellDefined identLeft groupIsAbelian (orderRespectsAddition 0<boundBelow below)) (prBoundBelow m (inequalityShrinkLeft N<m)))
+    ans m N<m | inr 0=am = exFalso (irreflexive {0G} (<WellDefined (Equivalence.symmetric eq 0=am) (Equivalence.reflexive eq) (SetoidPartialOrder.transitive pOrder (SetoidPartialOrder.transitive pOrder (<WellDefined identLeft (Equivalence.reflexive eq) (orderRespectsAddition 0<boundAbove (index (CauchyCompletion.elts a) m))) (prBoundAbove m (inequalityShrinkRight N<m))) above<0)))
+boundModulus' 0!=1 a | below , ((boundBelow , (0<boundBelow ,, (N , prBoundBelow))) ,, a-below<e) | above , ((boundAbove , (0<boundAbove ,, (Nabove , prBoundAbove))) ,, above-a<e) | inl (inr below<0) | inr 0=above = inverse below , ((N +N Nabove) , ans)
+  where
+    ans : (m : ℕ) → ((N +N Nabove) <N m) → abs (index (CauchyCompletion.elts a) m) < inverse below
+    ans m N<m with SetoidTotalOrder.totality tOrder 0R (index (CauchyCompletion.elts a) m)
+    ans m N<m | inl (inl 0<am) = exFalso (irreflexive {0G} (<WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq 0=above) (SetoidPartialOrder.transitive pOrder 0<am (SetoidPartialOrder.transitive pOrder (<WellDefined identLeft (Equivalence.reflexive eq) (orderRespectsAddition 0<boundAbove (index (CauchyCompletion.elts a) m))) (prBoundAbove m (inequalityShrinkRight N<m))))))
+    ans m N<m | inl (inr am<0) = ringSwapNegatives' (SetoidPartialOrder.transitive pOrder (<WellDefined identLeft groupIsAbelian (orderRespectsAddition 0<boundBelow below)) (prBoundBelow m (inequalityShrinkLeft N<m)))
+    ans m N<m | inr 0=am = <WellDefined 0=am (Equivalence.reflexive eq) (lemm2 _ below<0)
+boundModulus' 0!=1 a | below , ((boundBelow , ((boundBelowDiff ,, (Nb , ansBelow)))) ,, a-below<e) | above , ((bound , (0<bound ,, (N , ans))) ,, above-a<e) | inr 0=below = above , ((N +N Nb) , λ m N<m → SetoidPartialOrder.transitive pOrder (res m N<m) (ans m (inequalityShrinkLeft N<m)))
+  where
+    res : (m : ℕ) → (N +N Nb) <N m → (abs (index (CauchyCompletion.elts a) m)) < (bound + index (CauchyCompletion.elts a) m)
+    res m N<m with SetoidTotalOrder.totality tOrder 0R (index (CauchyCompletion.elts a) m)
+    res m N<m | inl (inl 0<am) = <WellDefined identLeft (Equivalence.reflexive eq) (orderRespectsAddition 0<bound (index (CauchyCompletion.elts a) m))
+    res m N<m | inl (inr am<0) = exFalso (irreflexive (<WellDefined (Equivalence.symmetric eq 0=below) (Equivalence.reflexive eq) (SetoidPartialOrder.transitive pOrder (SetoidPartialOrder.transitive pOrder (<WellDefined identLeft groupIsAbelian (orderRespectsAddition boundBelowDiff below)) (ansBelow m (inequalityShrinkRight N<m))) am<0)))
+    res m N<m | inr 0=am = <WellDefined 0=am (Equivalence.transitive eq (Equivalence.symmetric eq identRight) (+WellDefined (Equivalence.reflexive eq) 0=am)) 0<bound
+
+boundModulus : (0G ∼ 1R → False) → (a : CauchyCompletion) → Sg A (λ b → Sg ℕ (λ N → (m : ℕ) → (N <N m) → (abs (index (CauchyCompletion.elts a) m)) < b))
+boundModulus with SetoidTotalOrder.totality tOrder 0R 1R
+... | inl (inl 0<1) = λ _ → boundModulus' 0<1
+... | inl (inr 1<0) = exFalso (1<0False 1<0)
+... | inr (0=1) = λ bad → exFalso (bad 0=1)
diff --git a/Fields/CauchyCompletion/Comparison.agda b/Fields/CauchyCompletion/Comparison.agda
index 610a8c8..9995eef 100644
--- a/Fields/CauchyCompletion/Comparison.agda
+++ b/Fields/CauchyCompletion/Comparison.agda
@@ -39,77 +39,74 @@ shrinkInequality {a} {b} {c} (le x pr) = le (x +N b) (transitivity (applyEqualit
 shrinkInequality' : {a b c : ℕ} → a +N b <N c → b <N c
 shrinkInequality' {a} {b} {c} (le x pr) = le (x +N a) (transitivity (applyEquality succ (equalityCommutative (Semiring.+Associative ℕSemiring x _ _))) pr)
 
-_<C'_ : CauchyCompletion → A → Set (m ⊔ o)
-a <C' b = Sg A (λ ε → (0G < ε) && Sg ℕ (λ N → ((m : ℕ) → (N<m : N <N m) → (ε + index (CauchyCompletion.elts a) m) < b)))
+-- "<C rational", where the r indicates where the rational number goes
+_<Cr_ : CauchyCompletion → A → Set (m ⊔ o)
+a <Cr b = Sg A (λ ε → (0G < ε) && Sg ℕ (λ N → ((m : ℕ) → (N<m : N <N m) → (ε + index (CauchyCompletion.elts a) m) < b)))
 
-<C'WellDefinedRight : (a : CauchyCompletion) (b c : A) → b ∼ c → a <C' b → a <C' c
-<C'WellDefinedRight a b c b=c (ε , (0<e ,, (N , pr))) = ε , (0<e ,, (N , λ m N<m → <WellDefined (Equivalence.reflexive eq) b=c (pr m N<m)))
+<CrWellDefinedRight : (a : CauchyCompletion) (b c : A) → b ∼ c → a <Cr b → a <Cr c
+<CrWellDefinedRight a b c b=c (ε , (0<e ,, (N , pr))) = ε , (0<e ,, (N , λ m N<m → <WellDefined (Equivalence.reflexive eq) b=c (pr m N<m)))
 
-halfLess : (e/2 e : A) → (0<e : 0G < e) → (pr : e/2 + e/2 ∼ e) → e/2 < e
-halfLess e/2 e 0<e pr with halvePositive e/2 (<WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq pr) 0<e)
-... | 0<e/2 = <WellDefined identLeft pr (orderRespectsAddition 0<e/2 e/2)
+<CrWellDefinedLemma : (a b e/2 e : A) (0<e : 0G < e) (pr : e/2 + e/2 ∼ e) → abs (a + inverse b) < e/2 → (e/2 + b) < (e + a)
+<CrWellDefinedLemma a b e/2 e 0<e pr a-b<e with SetoidTotalOrder.totality tOrder 0G (a + inverse b)
+<CrWellDefinedLemma a b e/2 e 0<e pr a-b<e | inl (inl 0<a-b) = ringAddInequalities (halfLess e/2 e 0<e pr) (<WellDefined identLeft (Equivalence.transitive eq (Equivalence.symmetric eq +Associative) (Equivalence.transitive eq (+WellDefined (Equivalence.reflexive eq) invLeft) identRight)) (orderRespectsAddition 0<a-b b))
+<CrWellDefinedLemma a b e/2 e 0<e pr a-b<e | inl (inr a-b<0) = <WellDefined (Equivalence.transitive eq (+WellDefined (invContravariant (Ring.additiveGroup R)) groupIsAbelian) (Equivalence.transitive eq (Equivalence.transitive eq +Associative (+WellDefined (Equivalence.transitive eq (Equivalence.symmetric eq +Associative) (Equivalence.transitive eq (+WellDefined (invTwice additiveGroup b) invLeft) identRight)) (Equivalence.reflexive eq))) groupIsAbelian)) (Equivalence.transitive eq +Associative (+WellDefined pr (Equivalence.reflexive eq))) (orderRespectsAddition a-b<e (e/2 + a))
+<CrWellDefinedLemma a b e/2 e 0<e pr a-b<e | inr 0=a-b = <WellDefined (Equivalence.reflexive eq) (+WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq (transferToRight (Ring.additiveGroup R) (Equivalence.symmetric eq 0=a-b)))) (orderRespectsAddition (halfLess e/2 e 0<e pr) b)
 
-<C'WellDefinedLemma : (a b e/2 e : A) (0<e : 0G < e) (pr : e/2 + e/2 ∼ e) → abs (a + inverse b) < e/2 → (e/2 + b) < (e + a)
-<C'WellDefinedLemma a b e/2 e 0<e pr a-b<e with SetoidTotalOrder.totality tOrder 0G (a + inverse b)
-<C'WellDefinedLemma a b e/2 e 0<e pr a-b<e | inl (inl 0<a-b) = ringAddInequalities (halfLess e/2 e 0<e pr) (<WellDefined identLeft (Equivalence.transitive eq (Equivalence.symmetric eq +Associative) (Equivalence.transitive eq (+WellDefined (Equivalence.reflexive eq) invLeft) identRight)) (orderRespectsAddition 0<a-b b))
-<C'WellDefinedLemma a b e/2 e 0<e pr a-b<e | inl (inr a-b<0) = <WellDefined (Equivalence.transitive eq (+WellDefined (invContravariant (Ring.additiveGroup R)) groupIsAbelian) (Equivalence.transitive eq (Equivalence.transitive eq +Associative (+WellDefined (Equivalence.transitive eq (Equivalence.symmetric eq +Associative) (Equivalence.transitive eq (+WellDefined (invTwice additiveGroup b) invLeft) identRight)) (Equivalence.reflexive eq))) groupIsAbelian)) (Equivalence.transitive eq +Associative (+WellDefined pr (Equivalence.reflexive eq))) (orderRespectsAddition a-b<e (e/2 + a))
-<C'WellDefinedLemma a b e/2 e 0<e pr a-b<e | inr 0=a-b = <WellDefined (Equivalence.reflexive eq) (+WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq (transferToRight (Ring.additiveGroup R) (Equivalence.symmetric eq 0=a-b)))) (orderRespectsAddition (halfLess e/2 e 0<e pr) b)
-
-<C'WellDefinedLeft : (a b : CauchyCompletion) (c : A) → Setoid._∼_ cauchyCompletionSetoid a b → a <C' c → b <C' c
-<C'WellDefinedLeft a b c a=b (ε , (0<e ,, (N , pr))) with halve charNot2 ε
+<CrWellDefinedLeft : (a b : CauchyCompletion) (c : A) → Setoid._∼_ cauchyCompletionSetoid a b → a <Cr c → b <Cr c
+<CrWellDefinedLeft a b c a=b (ε , (0<e ,, (N , pr))) with halve charNot2 ε
 ... | e/2 , prE/2 with halvePositive e/2 (<WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq prE/2) 0<e)
 ... | 0<e/2 with a=b e/2 0<e/2
 ... | N2 , prN2 = e/2 , (0<e/2 ,, ((N +N N2) , ans))
   where
     ans : (m : ℕ) → (N<m : (N +N N2) <N m) → (e/2 + index (CauchyCompletion.elts b) m) < c
     ans m N<m with prN2 {m} (shrinkInequality' N<m)
-    ... | bl rewrite indexAndApply (CauchyCompletion.elts a) (map inverse (CauchyCompletion.elts b)) _+_ {m} | equalityCommutative (mapAndIndex (CauchyCompletion.elts b) inverse m) = SetoidPartialOrder.transitive pOrder (<C'WellDefinedLemma (index (CauchyCompletion.elts a) m) (index (CauchyCompletion.elts b) m) e/2 ε 0<e prE/2 bl) (pr m (shrinkInequality N<m))
+    ... | bl rewrite indexAndApply (CauchyCompletion.elts a) (map inverse (CauchyCompletion.elts b)) _+_ {m} | equalityCommutative (mapAndIndex (CauchyCompletion.elts b) inverse m) = SetoidPartialOrder.transitive pOrder (<CrWellDefinedLemma (index (CauchyCompletion.elts a) m) (index (CauchyCompletion.elts b) m) e/2 ε 0<e prE/2 bl) (pr m (shrinkInequality N<m))
 
-<C'WellDefined : (a b : CauchyCompletion) (c d : A) → Setoid._∼_ cauchyCompletionSetoid a b → c ∼ d → a <C' c → b <C' d
-<C'WellDefined a b c d a=b c=d a<c = <C'WellDefinedLeft a b d a=b (<C'WellDefinedRight a c d c=d a<c)
+<CrWellDefined : (a b : CauchyCompletion) (c d : A) → Setoid._∼_ cauchyCompletionSetoid a b → c ∼ d → a <Cr c → b <Cr d
+<CrWellDefined a b c d a=b c=d a<c = <CrWellDefinedLeft a b d a=b (<CrWellDefinedRight a c d c=d a<c)
 
-_<C''_ : A → CauchyCompletion → Set (m ⊔ o)
-a <C'' b = Sg A (λ ε → (0G < ε) && Sg ℕ (λ N → ((m : ℕ) → (N<m : N <N m) → (a + ε) < index (CauchyCompletion.elts b) m)))
+_r<C_ : A → CauchyCompletion → Set (m ⊔ o)
+a r<C b = Sg A (λ ε → (0G < ε) && Sg ℕ (λ N → ((m : ℕ) → (N<m : N <N m) → (a + ε) < index (CauchyCompletion.elts b) m)))
 
-<C''WellDefinedLeft : (a b : A) (c : CauchyCompletion) → (a ∼ b) → (a <C'' c) → b <C'' c
-<C''WellDefinedLeft a b c a=b (e , (0<e ,, (N , pr))) = e , (0<e ,, (N , λ m N<m → <WellDefined (+WellDefined a=b (Equivalence.reflexive eq)) (Equivalence.reflexive eq) (pr m N<m)))
+r<CWellDefinedLeft : (a b : A) (c : CauchyCompletion) → (a ∼ b) → (a r<C c) → b r<C c
+r<CWellDefinedLeft a b c a=b (e , (0<e ,, (N , pr))) = e , (0<e ,, (N , λ m N<m → <WellDefined (+WellDefined a=b (Equivalence.reflexive eq)) (Equivalence.reflexive eq) (pr m N<m)))
 
-<C''WellDefinedLemma : (a b c e e/2 : A) (_ : e/2 + e/2 ∼ e) (0<e : 0G < e) (_ : abs (a + inverse b) < e/2) (_ : (c + e) < a) → (c + e/2) < b
-<C''WellDefinedLemma a b c e e/2 prE/2 0<e pr c+e<a with SetoidTotalOrder.totality tOrder 0G (a + inverse b)
-<C''WellDefinedLemma a b c e e/2 prE/2 0<e pr c+e<a | inl (inl 0<a-b) = SetoidPartialOrder.transitive pOrder (<WellDefined (Equivalence.transitive eq (Equivalence.symmetric eq +Associative) (+WellDefined (Equivalence.reflexive eq) (Equivalence.transitive eq (+WellDefined (Equivalence.symmetric eq prE/2) (Equivalence.reflexive eq)) (Equivalence.transitive eq (Equivalence.transitive eq (Equivalence.symmetric eq +Associative) (+WellDefined (Equivalence.reflexive eq) invRight)) identRight)))) (Equivalence.reflexive eq) (orderRespectsAddition c+e<a (inverse e/2))) (<WellDefined (Equivalence.transitive eq +Associative (+WellDefined (Equivalence.transitive eq (Equivalence.symmetric eq +Associative) (Equivalence.transitive eq (+WellDefined (Equivalence.reflexive eq) invLeft) identRight)) (Equivalence.reflexive eq))) (Equivalence.transitive eq groupIsAbelian (Equivalence.transitive eq (Equivalence.symmetric eq +Associative) (Equivalence.transitive eq (+WellDefined (Equivalence.reflexive eq) (invLeft)) identRight))) (orderRespectsAddition pr (b + inverse e/2)))
-<C''WellDefinedLemma a b c e e/2 prE/2 0<e pr c+e<a | inl (inr a-b<0) = SetoidPartialOrder.transitive pOrder (SetoidPartialOrder.transitive pOrder (<WellDefined groupIsAbelian groupIsAbelian (orderRespectsAddition (halfLess e/2 e 0<e prE/2) c)) c+e<a) (<WellDefined (Equivalence.transitive eq (Equivalence.transitive eq (Equivalence.symmetric eq +Associative) (+WellDefined (Equivalence.reflexive eq) invLeft)) identRight) identLeft (orderRespectsAddition a-b<0 b))
-<C''WellDefinedLemma a b c e e/2 prE/2 0<e pr c+e<a | inr 0=a-b = SetoidPartialOrder.transitive pOrder (<WellDefined groupIsAbelian (Equivalence.reflexive eq) (orderRespectsAddition (halfLess e/2 e 0<e prE/2) c)) (<WellDefined (groupIsAbelian {c} {e}) (transferToRight additiveGroup (Equivalence.symmetric eq 0=a-b)) c+e<a)
+r<CWellDefinedLemma : (a b c e e/2 : A) (_ : e/2 + e/2 ∼ e) (0<e : 0G < e) (_ : abs (a + inverse b) < e/2) (_ : (c + e) < a) → (c + e/2) < b
+r<CWellDefinedLemma a b c e e/2 prE/2 0<e pr c+e<a with SetoidTotalOrder.totality tOrder 0G (a + inverse b)
+r<CWellDefinedLemma a b c e e/2 prE/2 0<e pr c+e<a | inl (inl 0<a-b) = SetoidPartialOrder.transitive pOrder (<WellDefined (Equivalence.transitive eq (Equivalence.symmetric eq +Associative) (+WellDefined (Equivalence.reflexive eq) (Equivalence.transitive eq (+WellDefined (Equivalence.symmetric eq prE/2) (Equivalence.reflexive eq)) (Equivalence.transitive eq (Equivalence.transitive eq (Equivalence.symmetric eq +Associative) (+WellDefined (Equivalence.reflexive eq) invRight)) identRight)))) (Equivalence.reflexive eq) (orderRespectsAddition c+e<a (inverse e/2))) (<WellDefined (Equivalence.transitive eq +Associative (+WellDefined (Equivalence.transitive eq (Equivalence.symmetric eq +Associative) (Equivalence.transitive eq (+WellDefined (Equivalence.reflexive eq) invLeft) identRight)) (Equivalence.reflexive eq))) (Equivalence.transitive eq groupIsAbelian (Equivalence.transitive eq (Equivalence.symmetric eq +Associative) (Equivalence.transitive eq (+WellDefined (Equivalence.reflexive eq) (invLeft)) identRight))) (orderRespectsAddition pr (b + inverse e/2)))
+r<CWellDefinedLemma a b c e e/2 prE/2 0<e pr c+e<a | inl (inr a-b<0) = SetoidPartialOrder.transitive pOrder (SetoidPartialOrder.transitive pOrder (<WellDefined groupIsAbelian groupIsAbelian (orderRespectsAddition (halfLess e/2 e 0<e prE/2) c)) c+e<a) (<WellDefined (Equivalence.transitive eq (Equivalence.transitive eq (Equivalence.symmetric eq +Associative) (+WellDefined (Equivalence.reflexive eq) invLeft)) identRight) identLeft (orderRespectsAddition a-b<0 b))
+r<CWellDefinedLemma a b c e e/2 prE/2 0<e pr c+e<a | inr 0=a-b = SetoidPartialOrder.transitive pOrder (<WellDefined groupIsAbelian (Equivalence.reflexive eq) (orderRespectsAddition (halfLess e/2 e 0<e prE/2) c)) (<WellDefined (groupIsAbelian {c} {e}) (transferToRight additiveGroup (Equivalence.symmetric eq 0=a-b)) c+e<a)
 
-<C''WellDefinedRight : (a b : CauchyCompletion) (c : A) → Setoid._∼_ cauchyCompletionSetoid a b → c <C'' a → c <C'' b
-<C''WellDefinedRight a b c a=b (e , (0<e ,, (N , pr))) with halve charNot2 e
+r<CWellDefinedRight : (a b : CauchyCompletion) (c : A) → Setoid._∼_ cauchyCompletionSetoid a b → c r<C a → c r<C b
+r<CWellDefinedRight a b c a=b (e , (0<e ,, (N , pr))) with halve charNot2 e
 ... | e/2 , prE/2 with halvePositive e/2 (<WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq prE/2) 0<e)
 ... | 0<e/2 with a=b e/2 0<e/2
 ... | N2 , prN2 = e/2 , (0<e/2 ,, ((N +N N2) , ans))
   where
     ans : (m : ℕ) → (N<m : (N +N N2) <N m) → (c + e/2) < index (CauchyCompletion.elts b) m
     ans m N<m with prN2 {m} (shrinkInequality' N<m)
-    ... | bl rewrite indexAndApply (CauchyCompletion.elts a) (map inverse (CauchyCompletion.elts b)) _+_ {m} | equalityCommutative (mapAndIndex (CauchyCompletion.elts b) inverse m) = <C''WellDefinedLemma (index (CauchyCompletion.elts a) m) (index (CauchyCompletion.elts b) m) c e e/2 prE/2 0<e bl (pr m (shrinkInequality N<m))
+    ... | bl rewrite indexAndApply (CauchyCompletion.elts a) (map inverse (CauchyCompletion.elts b)) _+_ {m} | equalityCommutative (mapAndIndex (CauchyCompletion.elts b) inverse m) = r<CWellDefinedLemma (index (CauchyCompletion.elts a) m) (index (CauchyCompletion.elts b) m) c e e/2 prE/2 0<e bl (pr m (shrinkInequality N<m))
 
 _<C_ : CauchyCompletion → CauchyCompletion → Set (m ⊔ o)
-a <C b = Sg A (λ i → (a <C' i) && (i <C'' b))
+a <C b = Sg A (λ i → (a <Cr i) && (i r<C b))
 
 <CWellDefined : {a b c d : CauchyCompletion} → Setoid._∼_ cauchyCompletionSetoid a b → Setoid._∼_ cauchyCompletionSetoid c d → a <C c → b <C d
-<CWellDefined {a} {b} {c} {d} a=b c=d (bound , (a<bound ,, bound<b)) = bound , (<C'WellDefinedLeft a b bound a=b a<bound ,, <C''WellDefinedRight c d bound c=d bound<b)
+<CWellDefined {a} {b} {c} {d} a=b c=d (bound , (a<bound ,, bound<b)) = bound , (<CrWellDefinedLeft a b bound a=b a<bound ,, r<CWellDefinedRight c d bound c=d bound<b)
 
-<C'Preserves : {a b : A} → a < b → injection a <C' b
-<C'Preserves {a} {b} a<b with dense charNot2 a<b
+<CrPreserves : {a b : A} → a < b → injection a <Cr b
+<CrPreserves {a} {b} a<b with dense charNot2 a<b
 ... | between , (a<between ,, between<b) = (between + inverse a) , (<WellDefined invRight (Equivalence.reflexive eq) (orderRespectsAddition a<between (inverse a)) ,, (0 , λ m _ → <WellDefined (Equivalence.transitive eq (Equivalence.symmetric eq identRight) (Equivalence.transitive eq (+WellDefined (Equivalence.reflexive eq) (ans a m)) +Associative)) (Equivalence.reflexive eq) between<b))
   where
     ans : (x : A) (m : ℕ) → 0G ∼ inverse x + index (constSequence x) m
     ans x m rewrite indexAndConst x m = Equivalence.symmetric eq invLeft
 
-<C''Preserves : {a b : A} → a < b → a <C'' injection b
-<C''Preserves {a} {b} a<b with dense charNot2 a<b
+r<CPreserves : {a b : A} → a < b → a r<C injection b
+r<CPreserves {a} {b} a<b with dense charNot2 a<b
 ... | between , (a<between ,, between<b) = (between + inverse a) , (<WellDefined invRight (Equivalence.reflexive eq) (orderRespectsAddition a<between (inverse a)) ,, (0 , λ m _ → <WellDefined (Equivalence.transitive eq (Equivalence.transitive eq (Equivalence.transitive eq (Equivalence.symmetric eq identRight) (+WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq invLeft))) +Associative) groupIsAbelian) (identityOfIndiscernablesLeft _∼_ (Equivalence.reflexive eq) (indexAndConst b m)) between<b))
 
 <CInherited : {a b : A} → a < b → (injection a) <C (injection b)
 <CInherited {a} {b} a<b with dense charNot2 a<b
-... | between , (a<between ,, between<b) = between , (<C'Preserves a<between ,, <C''Preserves between<b)
+... | between , (a<between ,, between<b) = between , (<CrPreserves a<between ,, r<CPreserves between<b)
 
 <CInherited' : {a b : A} → (injection a) <C (injection b) → a < b
 <CInherited' {a} {b} (bound , ((Na , (0<Na ,, (Na2 , prA))) ,, ((Nb , (0<Nb ,, (Nb2 , prB)))))) with prA (succ Na2) (le 0 refl)
diff --git a/Fields/CauchyCompletion/Multiplication.agda b/Fields/CauchyCompletion/Multiplication.agda
index c08b3aa..a5c30d7 100644
--- a/Fields/CauchyCompletion/Multiplication.agda
+++ b/Fields/CauchyCompletion/Multiplication.agda
@@ -29,6 +29,9 @@ open Field F
 open import Rings.Orders.Lemmas(order)
 open import Fields.CauchyCompletion.Definition order F
 open import Fields.CauchyCompletion.Setoid order F charNot2
+open import Fields.CauchyCompletion.Comparison order F charNot2
+open import Fields.CauchyCompletion.Addition order F charNot2
+open import Fields.CauchyCompletion.Approximation order F charNot2
 
 _*C_ : CauchyCompletion → CauchyCompletion → CauchyCompletion
 CauchyCompletion.elts (record { elts = a ; converges = aConv } *C record { elts = b ; converges = bConv }) = apply _*_ a b
@@ -42,11 +45,61 @@ CauchyCompletion.converges (record { elts = a ; converges = aConv } *C record {
     ans : {m : ℕ} → 0 <N m → abs (index (apply _+_ (CauchyCompletion.elts (a *C b)) (map inverse (CauchyCompletion.elts (b *C a)))) m) < ε
     ans {m} 0<m rewrite indexAndApply (apply _*_ (CauchyCompletion.elts a) (CauchyCompletion.elts b)) (map inverse (apply _*_ (CauchyCompletion.elts b) (CauchyCompletion.elts a))) _+_ {m} | indexAndApply (CauchyCompletion.elts a) (CauchyCompletion.elts b) _*_ {m} | equalityCommutative (mapAndIndex (apply _*_ (CauchyCompletion.elts b) (CauchyCompletion.elts a)) inverse m) | indexAndApply (CauchyCompletion.elts b) (CauchyCompletion.elts a) _*_ {m} = <WellDefined (Equivalence.symmetric eq (Equivalence.transitive eq (absWellDefined _ _ foo) (identityOfIndiscernablesRight _∼_ (Equivalence.reflexive eq) (absZero order)))) (Equivalence.reflexive eq) 0<e
 
-multiplicationWellDefinedLeft : (a b c : CauchyCompletion) → Setoid._∼_ cauchyCompletionSetoid a b → Setoid._∼_ cauchyCompletionSetoid (a *C c) (b *C c)
-multiplicationWellDefinedLeft a b c a=b ε 0<e = 0 , ans
+absBoundedImpliesBounded : {a b : A} → abs a < b → a < b
+absBoundedImpliesBounded {a} {b} a<b with SetoidTotalOrder.totality tOrder 0G a
+absBoundedImpliesBounded {a} {b} a<b | inl (inl x) = a<b
+absBoundedImpliesBounded {a} {b} a<b | inl (inr x) = SetoidPartialOrder.transitive pOrder x (SetoidPartialOrder.transitive pOrder (lemm2 a x) a<b)
+absBoundedImpliesBounded {a} {b} a<b | inr x = a<b
+
+multiplicationWellDefinedLeft' : (0!=1 : 0R ∼ 1R → False) (a b c : CauchyCompletion) → Setoid._∼_ cauchyCompletionSetoid a b → Setoid._∼_ cauchyCompletionSetoid (a *C c) (b *C c)
+multiplicationWellDefinedLeft' 0!=1 a b c a=b ε 0<e = N , ans
   where
-    ans : {m : ℕ} → 0 <N m → abs (index (apply _+_ (apply _*_ (CauchyCompletion.elts a) (CauchyCompletion.elts c)) (map inverse (apply _*_ (CauchyCompletion.elts b) (CauchyCompletion.elts c)))) m) < ε
-    ans {m} N<m rewrite indexAndApply (apply _*_ (CauchyCompletion.elts a) (CauchyCompletion.elts c)) (map inverse (apply _*_ (CauchyCompletion.elts b) (CauchyCompletion.elts c))) _+_ {m} | equalityCommutative (mapAndIndex (apply _*_ (CauchyCompletion.elts b) (CauchyCompletion.elts c)) inverse m) | indexAndApply (CauchyCompletion.elts b) (CauchyCompletion.elts c) _*_ {m} | indexAndApply (CauchyCompletion.elts a) (CauchyCompletion.elts c) _*_ {m} = {!!}
+    cBound : A
+    cBound = ?
+    0<cBound : 0G < cBound
+    0<cBound = {!!}
+    e/c : A
+    e/c with allInvertible cBound (λ pr → irreflexive (<WellDefined (Equivalence.reflexive eq) pr 0<cBound))
+    ... | (1/c , _) = ε * 1/c
+    e/cPr : e/c * cBound ∼ ε
+    e/cPr with allInvertible cBound (λ pr → irreflexive (<WellDefined (Equivalence.reflexive eq) pr 0<cBound))
+    ... | (1/c , pr) = Equivalence.transitive eq (Equivalence.transitive eq (Equivalence.transitive eq (Equivalence.symmetric eq *Associative) (*WellDefined (Equivalence.reflexive eq) pr)) *Commutative) (identIsIdent)
+    0<e/c : 0G < e/c
+    0<e/c = ringCanCancelPositive {0G} {e/c} 0<cBound (<WellDefined (Equivalence.symmetric eq (Equivalence.transitive eq *Commutative timesZero)) (Equivalence.symmetric eq e/cPr) 0<e)
+    abBound : ℕ
+    abBound with a=b e/c 0<e/c
+    ... | Na=b , _ = Na=b
+    abPr : {m : ℕ} → (abBound <N m) → abs (index (apply _+_ (CauchyCompletion.elts a) (map inverse (CauchyCompletion.elts b))) m) < e/c
+    abPr with a=b e/c 0<e/c
+    ... | Na=b , pr = pr
+    N : ℕ
+    N = abBound +N {!!}
+    cBounded : (m : ℕ) → (N <N m) → abs (index (CauchyCompletion.elts c) m) < cBound
+    cBounded m N<m = {!SetoidPartialOrder.transitive pOrder !}
+    a-bSmall : (m : ℕ) → N <N m → abs ((index (CauchyCompletion.elts a) m) + inverse (index (CauchyCompletion.elts b) m)) < e/c
+    a-bSmall m N<m with abPr {m} (inequalityShrinkLeft N<m)
+    ... | f rewrite indexAndApply (CauchyCompletion.elts a) (map inverse (CauchyCompletion.elts b)) _+_ {m} | equalityCommutative (mapAndIndex (CauchyCompletion.elts b) inverse m) = f
+    ans : {m : ℕ} → N <N m → abs (index (apply _+_ (apply _*_ (CauchyCompletion.elts a) (CauchyCompletion.elts c)) (map inverse (apply _*_ (CauchyCompletion.elts b) (CauchyCompletion.elts c)))) m) < ε
+    ans {m} N<m rewrite indexAndApply (apply _*_ (CauchyCompletion.elts a) (CauchyCompletion.elts c)) (map inverse (apply _*_ (CauchyCompletion.elts b) (CauchyCompletion.elts c))) _+_ {m} | equalityCommutative (mapAndIndex (apply _*_ (CauchyCompletion.elts b) (CauchyCompletion.elts c)) inverse m) | indexAndApply (CauchyCompletion.elts b) (CauchyCompletion.elts c) _*_ {m} | indexAndApply (CauchyCompletion.elts a) (CauchyCompletion.elts c) _*_ {m} = <WellDefined (absWellDefined _ _ (+WellDefined (Equivalence.reflexive eq) (ringMinusExtracts' R))) (Equivalence.reflexive eq) (<WellDefined (absWellDefined ((index (CauchyCompletion.elts a) m + inverse (index (CauchyCompletion.elts b) m)) * index (CauchyCompletion.elts c) m) _ (Equivalence.transitive eq (Equivalence.transitive eq *Commutative *DistributesOver+) (+WellDefined *Commutative *Commutative))) (Equivalence.reflexive eq) (<WellDefined (Equivalence.symmetric eq (absRespectsTimes _ _)) (Equivalence.reflexive eq) (<WellDefined (Equivalence.reflexive eq) e/cPr (ans' (index (CauchyCompletion.elts a) m) (index (CauchyCompletion.elts b) m) (index (CauchyCompletion.elts c) m) (a-bSmall m N<m) (cBounded m N<m)))))
+      where
+        ans' : (a b c : A) → abs (a + inverse b) < e/c → abs c < cBound → (abs (a + inverse b) * abs c) < (e/c * cBound)
+        ans' a b c a-b<e/c c<bound with SetoidTotalOrder.totality tOrder 0R c
+        ans' a b c a-b<e/c c<bound | inl (inl 0<c) with totality 0G (a + inverse b)
+        ans' a b c a-b<e/c c<bound | inl (inl 0<c) | inl (inl 0<a-b) = ringMultiplyPositives 0<a-b 0<c a-b<e/c c<bound
+        ans' a b c a-b<e/c c<bound | inl (inl 0<c) | inl (inr a-b<0) = ringMultiplyPositives (lemm2 (a + inverse b) a-b<0) 0<c a-b<e/c c<bound
+        ans' a b c a-b<e/c c<bound | inl (inl 0<c) | inr 0=a-b = <WellDefined (Equivalence.symmetric eq (Equivalence.transitive eq (*WellDefined (Equivalence.symmetric eq 0=a-b) (Equivalence.reflexive eq)) (Equivalence.transitive eq *Commutative timesZero))) (Equivalence.reflexive eq) (orderRespectsMultiplication 0<e/c 0<cBound)
+        ans' a b c a-b<e/c c<bound | inl (inr c<0) with totality 0G (a + inverse b)
+        ans' a b c a-b<e/c c<bound | inl (inr c<0) | inl (inl 0<a-b) = ringMultiplyPositives 0<a-b (lemm2 c c<0) a-b<e/c c<bound
+        ans' a b c a-b<e/c c<bound | inl (inr c<0) | inl (inr a-b<0) = ringMultiplyPositives (lemm2 (a + inverse b) a-b<0) (lemm2 c c<0) a-b<e/c c<bound
+        ans' a b c a-b<e/c c<bound | inl (inr c<0) | inr 0=a-b = <WellDefined (Equivalence.symmetric eq (Equivalence.transitive eq (*WellDefined (Equivalence.symmetric eq 0=a-b) (Equivalence.reflexive eq)) (Equivalence.transitive eq *Commutative timesZero))) (Equivalence.reflexive eq) (orderRespectsMultiplication 0<e/c 0<cBound)
+        ans' a b c a-b<e/c c<bound | inr 0=c = <WellDefined (Equivalence.symmetric eq (Equivalence.transitive eq (*WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq 0=c)) timesZero)) (Equivalence.reflexive eq) (orderRespectsMultiplication 0<e/c 0<cBound)
+
+
+multiplicationWellDefinedLeft : (a b c : CauchyCompletion) → Setoid._∼_ cauchyCompletionSetoid a b → Setoid._∼_ cauchyCompletionSetoid (a *C c) (b *C c)
+multiplicationWellDefinedLeft with SetoidTotalOrder.totality tOrder 0R 1R
+... | inl (inl 0<1') = multiplicationWellDefinedLeft' (λ pr → irreflexive {0G} (<WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq pr) 0<1'))
+... | inl (inr 1<0) = multiplicationWellDefinedLeft' (λ pr → irreflexive {0G} (<WellDefined (Equivalence.symmetric eq pr) (Equivalence.reflexive eq) 1<0))
+... | inr (0=1) = λ a b c a=b → Equivalence.transitive (Setoid.eq cauchyCompletionSetoid) {a *C c} {injection 0G} {b *C c} (Equivalence.symmetric (Setoid.eq cauchyCompletionSetoid) {injection 0G} {a *C c} (trivialIfInputTrivial 0=1 (a *C c))) (trivialIfInputTrivial 0=1 (b *C c))
 
 multiplicationPreservedLeft : {a b : A} {c : CauchyCompletion} → (a ∼ b) → Setoid._∼_ cauchyCompletionSetoid (injection a *C c) (injection b *C c)
 multiplicationPreservedLeft {a} {b} {c} a=b = multiplicationWellDefinedLeft (injection a) (injection b) c (injectionPreservesSetoid a b a=b)
diff --git a/Fields/CauchyCompletion/Setoid.agda b/Fields/CauchyCompletion/Setoid.agda
index 4900760..954e359 100644
--- a/Fields/CauchyCompletion/Setoid.agda
+++ b/Fields/CauchyCompletion/Setoid.agda
@@ -131,3 +131,6 @@ additionHom x y ε 0<e = 0 , ans
 CInjection : SetoidInjection S cauchyCompletionSetoid injection
 SetoidInjection.wellDefined CInjection {x} {y} x=y = injectionPreservesSetoid x y x=y
 SetoidInjection.injective CInjection {x} {y} x=y = injectionPreservesSetoid' x y x=y
+
+trivialIfInputTrivial : (0R ∼ 1R) → (a : CauchyCompletion) → Setoid._∼_ cauchyCompletionSetoid (injection 0R) a
+trivialIfInputTrivial 0=1 a ε 0<e = exFalso (irreflexive {0G} (<WellDefined (Equivalence.reflexive eq) (oneZeroImpliesAllZero R 0=1) 0<e))
diff --git a/Fields/Orders/Lemmas.agda b/Fields/Orders/Lemmas.agda
index 4e3fd39..4905229 100644
--- a/Fields/Orders/Lemmas.agda
+++ b/Fields/Orders/Lemmas.agda
@@ -46,3 +46,7 @@ halveInequality' x y 1/2 pr1/2 x<2y with halveInequality (inverse y) (inverse x)
 dense : (charNot2 : ((1R + 1R) ∼ 0R) → False) {x y : A} → (x < y) → Sg A (λ i → (x < i) && (i < y))
 dense charNot2 {x} {y} x<y with halve charNot2 1R
 dense charNot2 {x} {y} x<y | 1/2 , pr1/2 = ((x + y) * 1/2) , (halveInequality x (x + y) 1/2 pr1/2 (<WellDefined (Equivalence.reflexive eq) groupIsAbelian (orderRespectsAddition x<y x)) ,, halveInequality' (x + y) y 1/2 pr1/2 (orderRespectsAddition x<y y))
+
+halfLess : (e/2 e : A) → (0<e : 0G < e) → (pr : e/2 + e/2 ∼ e) → e/2 < e
+halfLess e/2 e 0<e pr with halvePositive e/2 (<WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq pr) 0<e)
+... | 0<e/2 = <WellDefined identLeft pr (orderRespectsAddition 0<e/2 e/2)
diff --git a/Numbers/Naturals/Naturals.agda b/Numbers/Naturals/Naturals.agda
index ab21781..202a000 100644
--- a/Numbers/Naturals/Naturals.agda
+++ b/Numbers/Naturals/Naturals.agda
@@ -560,3 +560,6 @@ module Numbers.Naturals.Naturals where
 
   inequalityShrinkLeft : {a b c : ℕ} → a +N b <N c → a <N c
   inequalityShrinkLeft {a} {b} {c} (le x proof) = le (x +N b) (transitivity (applyEquality succ (transitivity (additionNIsAssociative x b a) (applyEquality (x +N_) (additionNIsCommutative b a)))) proof)
+
+  <NWellDefined' : {a b c d : ℕ} → a ≡ c → b ≡ d → a <N b → c <N d
+  <NWellDefined' {a} {b} {c} {d} a=c b=d a<b rewrite a=c | b=d = a<b
diff --git a/Rings/Orders/Lemmas.agda b/Rings/Orders/Lemmas.agda
index 5fdc6f2..1558541 100644
--- a/Rings/Orders/Lemmas.agda
+++ b/Rings/Orders/Lemmas.agda
@@ -138,6 +138,9 @@ ringCanMultiplyByPositive {x} {y} {c} 0<c x<y = SetoidPartialOrder.<WellDefined
     q' : (x * c) < ((y * c) + 0R)
     q' = SetoidPartialOrder.<WellDefined pOrder (Group.identLeft additiveGroup) (Equivalence.transitive eq (symmetric (Group.+Associative additiveGroup)) (Group.+WellDefined additiveGroup reflexive (Group.invLeft additiveGroup))) q
 
+ringMultiplyPositives : {x y a b : A} → 0R < x → 0R < a → (x < y) → (a < b) → (x * a) < (y * b)
+ringMultiplyPositives {x} {y} {a} {b} 0<x 0<a x<y a<b = SetoidPartialOrder.transitive pOrder (ringCanMultiplyByPositive 0<a x<y) (<WellDefined *Commutative *Commutative (ringCanMultiplyByPositive (SetoidPartialOrder.transitive pOrder 0<x x<y) a<b))
+
 ringCanCancelPositive : {x y c : A} → (Ring.0R R) < c → (x * c) < (y * c) → x < y
 ringCanCancelPositive {x} {y} {c} 0<c xc<yc = SetoidPartialOrder.<WellDefined pOrder (Group.identLeft additiveGroup) (Equivalence.transitive eq (symmetric (Group.+Associative additiveGroup)) (Equivalence.transitive eq (Group.+WellDefined additiveGroup reflexive (Group.invLeft additiveGroup)) (Group.identRight additiveGroup))) q''
   where
@@ -328,3 +331,13 @@ halvePositive a 0<2a | inr x = exFalso (irreflexive {0G} (<WellDefined (Equivale
 0<1 0!=1 | inl (inl x) = x
 0<1 0!=1 | inl (inr x) = <WellDefined (Equivalence.reflexive eq) (Equivalence.transitive eq twoNegativesTimes identIsIdent) (orderRespectsMultiplication (lemm2 1R x) (lemm2 1R x))
 0<1 0!=1 | inr x = exFalso (0!=1 x)
+
+addingAbsCannotShrink : {a b : A} → 0G < b → 0G < ((abs a) + b)
+addingAbsCannotShrink {a} {b} 0<b with SetoidTotalOrder.totality tOrder 0G a
+addingAbsCannotShrink {a} {b} 0<b | inl (inl x) = <WellDefined identLeft (Equivalence.reflexive eq) (ringAddInequalities x 0<b)
+addingAbsCannotShrink {a} {b} 0<b | inl (inr x) = <WellDefined identLeft (Equivalence.reflexive eq) (ringAddInequalities (lemm2 a x) 0<b)
+addingAbsCannotShrink {a} {b} 0<b | inr x = <WellDefined (Equivalence.reflexive eq) (Equivalence.transitive eq (Equivalence.symmetric eq identLeft) (+WellDefined x (Equivalence.reflexive eq))) 0<b
+
+1<0False : (1R < 0R) → False
+1<0False 1<0 with orderRespectsMultiplication (lemm2 _ 1<0) (lemm2 _ 1<0)
+... | bl = exFalso (irreflexive (SetoidPartialOrder.transitive pOrder 1<0 (<WellDefined (Equivalence.reflexive eq) (Equivalence.transitive eq (twoNegativesTimes) identIsIdent) bl)))