diff --git a/src/commutative-algebra/commutative-rings.lagda.md b/src/commutative-algebra/commutative-rings.lagda.md
index a12e07d1fe..2fd1976b3d 100644
--- a/src/commutative-algebra/commutative-rings.lagda.md
+++ b/src/commutative-algebra/commutative-rings.lagda.md
@@ -200,6 +200,13 @@ module _
   right-subtraction-Commutative-Ring =
     right-subtraction-Ring ring-Commutative-Ring
 
+  ap-right-subtraction-Commutative-Ring :
+    {x x' y y' : type-Commutative-Ring} → x ＝ x' → y ＝ y' →
+    right-subtraction-Commutative-Ring x y ＝
+    right-subtraction-Commutative-Ring x' y'
+  ap-right-subtraction-Commutative-Ring =
+    ap-right-subtraction-Ring ring-Commutative-Ring
+
   is-section-right-subtraction-Commutative-Ring :
     (x : type-Commutative-Ring) →
     ( add-Commutative-Ring' x ∘
@@ -659,3 +666,20 @@ module _
   preserves-concat-add-list-Commutative-Ring =
     preserves-concat-add-list-Ring ring-Commutative-Ring
 ```
+
+### The sum of `x - y` and `y - z` is `x - z`
+
+```agda
+module _
+  {l : Level} (R : Commutative-Ring l)
+  where
+
+  add-right-subtraction-Commutative-Ring :
+    (x y z : type-Commutative-Ring R) →
+    add-Commutative-Ring R
+      ( right-subtraction-Commutative-Ring R x y)
+      ( right-subtraction-Commutative-Ring R y z) ＝
+    right-subtraction-Commutative-Ring R x z
+  add-right-subtraction-Commutative-Ring =
+    add-right-subtraction-Ab (ab-Commutative-Ring R)
+```
diff --git a/src/commutative-algebra/geometric-sequences-commutative-rings.lagda.md b/src/commutative-algebra/geometric-sequences-commutative-rings.lagda.md
index 9343e05ed8..5af1cfd3a2 100644
--- a/src/commutative-algebra/geometric-sequences-commutative-rings.lagda.md
+++ b/src/commutative-algebra/geometric-sequences-commutative-rings.lagda.md
@@ -10,7 +10,10 @@ module commutative-algebra.geometric-sequences-commutative-rings where
 open import commutative-algebra.commutative-rings
 open import commutative-algebra.commutative-semirings
 open import commutative-algebra.geometric-sequences-commutative-semirings
+open import commutative-algebra.groups-of-units-commutative-rings
+open import commutative-algebra.invertible-elements-commutative-rings
 open import commutative-algebra.powers-of-elements-commutative-rings
+open import commutative-algebra.sums-of-finite-sequences-of-elements-commutative-rings
 
 open import elementary-number-theory.natural-numbers
 
@@ -288,6 +291,11 @@ module _
 ```agda
 module _
   {l : Level} (R : Commutative-Ring l) (a r : type-Commutative-Ring R)
+  (let _*R_ = mul-Commutative-Ring R)
+  (let _+R_ = add-Commutative-Ring R)
+  (let _-R_ = right-subtraction-Commutative-Ring R)
+  (let zero-R = zero-Commutative-Ring R)
+  (let one-R = one-Commutative-Ring R)
   where
 
   abstract
@@ -307,4 +315,141 @@ module _
         ( commutative-semiring-Commutative-Ring R)
         ( a)
         ( r)
+
+  abstract
+    compute-sum-standard-geometric-fin-sequence-Commutative-Ring :
+      (H :
+        is-invertible-element-Commutative-Ring R
+          ( right-subtraction-Commutative-Ring R (one-Commutative-Ring R) r)) →
+      (n : ℕ) →
+      sum-standard-geometric-fin-sequence-Commutative-Ring R a r n ＝
+      mul-Commutative-Ring R
+        ( mul-Commutative-Ring R
+          ( a)
+          ( inv-is-invertible-element-Commutative-Ring R H))
+        ( right-subtraction-Commutative-Ring R
+          ( one-Commutative-Ring R)
+          ( power-Commutative-Ring R n r))
+    compute-sum-standard-geometric-fin-sequence-Commutative-Ring
+      (1/⟨1-r⟩ , H) 0 =
+      inv
+        ( equational-reasoning
+          (a *R 1/⟨1-r⟩) *R (one-R -R one-R)
+          ＝ (a *R 1/⟨1-r⟩) *R zero-R
+            by
+              ap-mul-Commutative-Ring R
+                ( refl)
+                ( right-inverse-law-add-Commutative-Ring R one-R)
+          ＝ zero-R
+            by right-zero-law-mul-Commutative-Ring R _)
+    compute-sum-standard-geometric-fin-sequence-Commutative-Ring
+      (1/⟨1-r⟩ , H) (succ-ℕ n) =
+      equational-reasoning
+        sum-standard-geometric-fin-sequence-Commutative-Ring R a r (succ-ℕ n)
+        ＝
+          sum-standard-geometric-fin-sequence-Commutative-Ring R a r n +R
+          seq-standard-geometric-sequence-Commutative-Ring R a r n
+          by
+            cons-sum-fin-sequence-type-Commutative-Ring R
+              ( n)
+              ( standard-geometric-fin-sequence-Commutative-Ring R
+                ( a)
+                ( r)
+                ( succ-ℕ n))
+              ( refl)
+        ＝
+          ( (a *R 1/⟨1-r⟩) *R (one-R -R power-Commutative-Ring R n r)) +R
+          ( a *R power-Commutative-Ring R n r)
+          by
+            ap-add-Commutative-Ring R
+              ( compute-sum-standard-geometric-fin-sequence-Commutative-Ring
+                ( 1/⟨1-r⟩ , H)
+                ( n))
+              ( inv
+                ( htpy-mul-pow-standard-geometric-sequence-Commutative-Ring R
+                  ( a)
+                  ( r)
+                  ( n)))
+        ＝
+          ( a *R (1/⟨1-r⟩ *R (one-R -R power-Commutative-Ring R n r))) +R
+          ( a *R (one-R *R power-Commutative-Ring R n r))
+          by
+            ap-add-Commutative-Ring R
+              ( associative-mul-Commutative-Ring R _ _ _)
+              ( ap-mul-Commutative-Ring R
+                ( refl)
+                ( inv (left-unit-law-mul-Commutative-Ring R _)))
+        ＝
+          a *R
+          ( (1/⟨1-r⟩ *R (one-R -R power-Commutative-Ring R n r)) +R
+            (one-R *R power-Commutative-Ring R n r))
+          by inv (left-distributive-mul-add-Commutative-Ring R a _ _)
+        ＝
+          a *R
+          ( ( 1/⟨1-r⟩ *R (one-R -R power-Commutative-Ring R n r)) +R
+            ( (1/⟨1-r⟩ *R (one-R -R r)) *R power-Commutative-Ring R n r))
+            by
+              ap-mul-Commutative-Ring R
+                ( refl)
+                ( ap-add-Commutative-Ring R
+                  ( refl)
+                  ( ap-mul-Commutative-Ring R (inv (pr2 H)) refl))
+        ＝
+          a *R
+          ( ( 1/⟨1-r⟩ *R (one-R -R power-Commutative-Ring R n r)) +R
+            ( 1/⟨1-r⟩ *R ((one-R -R r) *R power-Commutative-Ring R n r)))
+          by
+            ap-mul-Commutative-Ring R
+              ( refl)
+              ( ap-add-Commutative-Ring R
+                ( refl)
+                ( associative-mul-Commutative-Ring R _ _ _))
+        ＝
+          a *R
+          ( 1/⟨1-r⟩ *R
+            ( ( one-R -R power-Commutative-Ring R n r) +R
+              ( (one-R -R r) *R power-Commutative-Ring R n r)))
+          by
+            ap-mul-Commutative-Ring R
+              ( refl)
+              ( inv (left-distributive-mul-add-Commutative-Ring R _ _ _))
+        ＝
+          ( a *R 1/⟨1-r⟩) *R
+          ( ( one-R -R power-Commutative-Ring R n r) +R
+            ( (one-R -R r) *R power-Commutative-Ring R n r))
+          by inv (associative-mul-Commutative-Ring R _ _ _)
+        ＝
+          ( a *R 1/⟨1-r⟩) *R
+          ( ( one-R -R power-Commutative-Ring R n r) +R
+            ( (one-R *R power-Commutative-Ring R n r) -R
+              (r *R power-Commutative-Ring R n r)))
+          by
+            ap-mul-Commutative-Ring R
+              ( refl)
+              ( ap-add-Commutative-Ring R
+                ( refl)
+                ( right-distributive-mul-right-subtraction-Commutative-Ring R
+                  ( _)
+                  ( _)
+                  ( _)))
+        ＝
+          ( a *R 1/⟨1-r⟩) *R
+          ( ( one-R -R power-Commutative-Ring R n r) +R
+            ( power-Commutative-Ring R n r -R
+              power-Commutative-Ring R (succ-ℕ n) r))
+          by
+            ap-mul-Commutative-Ring R
+              ( refl)
+              ( ap-add-Commutative-Ring R
+                ( refl)
+                ( ap-right-subtraction-Commutative-Ring R
+                  ( left-unit-law-mul-Commutative-Ring R _)
+                  ( inv (power-succ-Commutative-Ring' R n r))))
+        ＝
+          ( a *R 1/⟨1-r⟩) *R
+          ( one-R -R power-Commutative-Ring R (succ-ℕ n) r)
+          by
+            ap-mul-Commutative-Ring R
+              ( refl)
+              ( add-right-subtraction-Commutative-Ring R _ _ _)
 ```
diff --git a/src/elementary-number-theory/geometric-sequences-rational-numbers.lagda.md b/src/elementary-number-theory/geometric-sequences-rational-numbers.lagda.md
index 07004973a8..5e81a68f07 100644
--- a/src/elementary-number-theory/geometric-sequences-rational-numbers.lagda.md
+++ b/src/elementary-number-theory/geometric-sequences-rational-numbers.lagda.md
@@ -30,6 +30,7 @@ open import elementary-number-theory.ring-of-rational-numbers
 open import elementary-number-theory.strict-inequality-rational-numbers
 
 open import foundation.binary-transport
+open import foundation.dependent-pair-types
 open import foundation.function-extensionality
 open import foundation.identity-types
 open import foundation.negated-equality
@@ -111,102 +112,14 @@ module _
     compute-sum-standard-geometric-fin-sequence-ℚ :
       (n : ℕ) →
       sum-standard-geometric-fin-sequence-ℚ a r n ＝
-      ( a *ℚ
-        ( (one-ℚ -ℚ power-ℚ n r) *ℚ
-          rational-inv-ℚˣ (invertible-diff-neq-ℚ r one-ℚ r≠1)))
-    compute-sum-standard-geometric-fin-sequence-ℚ 0 =
-      inv
-        ( equational-reasoning
-          a *ℚ ((one-ℚ -ℚ one-ℚ) *ℚ _)
-          ＝ a *ℚ (zero-ℚ *ℚ _)
-            by
-              ap-mul-ℚ
-                ( refl)
-                ( ap-mul-ℚ (right-inverse-law-add-ℚ one-ℚ) refl)
-          ＝ a *ℚ zero-ℚ
-            by ap-mul-ℚ refl (left-zero-law-mul-ℚ _)
-          ＝ zero-ℚ
-            by right-zero-law-mul-ℚ a)
-    compute-sum-standard-geometric-fin-sequence-ℚ (succ-ℕ n) =
-      let
-        1/⟨1-r⟩ = rational-inv-ℚˣ (invertible-diff-neq-ℚ r one-ℚ r≠1)
-      in
-        equational-reasoning
-          sum-standard-geometric-fin-sequence-ℚ a r (succ-ℕ n)
-          ＝
-            sum-standard-geometric-fin-sequence-ℚ a r n +ℚ
-            seq-standard-geometric-sequence-ℚ a r n
-            by
-              cons-sum-fin-sequence-type-Commutative-Ring
-                ( commutative-ring-ℚ)
-                ( n)
-                ( _)
-                ( refl)
-          ＝
-            ( a *ℚ
-              ( (one-ℚ -ℚ power-ℚ n r) *ℚ 1/⟨1-r⟩)) +ℚ
-            ( a *ℚ power-ℚ n r)
-            by
-              ap-add-ℚ
-                ( compute-sum-standard-geometric-fin-sequence-ℚ n)
-                ( compute-standard-geometric-sequence-ℚ a r n)
-          ＝
-            a *ℚ
-            (((one-ℚ -ℚ power-ℚ n r) *ℚ 1/⟨1-r⟩) +ℚ power-ℚ n r)
-            by inv (left-distributive-mul-add-ℚ a _ _)
-          ＝
-            a *ℚ
-            ( (((one-ℚ -ℚ power-ℚ n r) *ℚ 1/⟨1-r⟩) +ℚ
-              (power-ℚ n r *ℚ (one-ℚ -ℚ r)) *ℚ 1/⟨1-r⟩))
-            by
-              ap-mul-ℚ
-                ( refl)
-                ( ap-add-ℚ
-                  ( refl)
-                  ( inv
-                    ( cancel-right-mul-div-ℚˣ _
-                      ( invertible-diff-neq-ℚ r one-ℚ r≠1))))
-          ＝
-            a *ℚ
-            ( ( (one-ℚ -ℚ power-ℚ n r) +ℚ (power-ℚ n r *ℚ (one-ℚ -ℚ r))) *ℚ
-              1/⟨1-r⟩)
-            by
-              ap-mul-ℚ
-                ( refl)
-                ( inv (right-distributive-mul-add-ℚ _ _ 1/⟨1-r⟩))
-          ＝
-            a *ℚ
-            ( ( one-ℚ -ℚ power-ℚ n r +ℚ
-                ((power-ℚ n r *ℚ one-ℚ) -ℚ (power-ℚ n r *ℚ r))) *ℚ
-              1/⟨1-r⟩)
-            by
-              ap-mul-ℚ
-                ( refl)
-                ( ap-mul-ℚ
-                  ( ap-add-ℚ refl (left-distributive-mul-diff-ℚ _ _ _))
-                  ( refl))
-          ＝
-            a *ℚ
-            ( ( one-ℚ -ℚ power-ℚ n r +ℚ
-                ((power-ℚ n r -ℚ power-ℚ (succ-ℕ n) r))) *ℚ
-              1/⟨1-r⟩)
-            by
-              ap-mul-ℚ
-                ( refl)
-                ( ap-mul-ℚ
-                  ( ap-add-ℚ
-                    ( refl)
-                    ( ap-diff-ℚ
-                      ( right-unit-law-mul-ℚ _)
-                      ( inv (power-succ-ℚ n r))))
-                  ( refl))
-          ＝ a *ℚ ((one-ℚ -ℚ power-ℚ (succ-ℕ n) r) *ℚ 1/⟨1-r⟩)
-            by
-              ap-mul-ℚ
-                ( refl)
-                ( ap-mul-ℚ
-                  ( mul-right-div-Group group-add-ℚ _ _ _)
-                  ( refl))
+      ( (a *ℚ rational-inv-ℚˣ (invertible-diff-neq-ℚ r one-ℚ r≠1)) *ℚ
+        (one-ℚ -ℚ power-ℚ n r))
+    compute-sum-standard-geometric-fin-sequence-ℚ =
+      compute-sum-standard-geometric-fin-sequence-Commutative-Ring
+        ( commutative-ring-ℚ)
+        ( a)
+        ( r)
+        ( pr2 (invertible-diff-neq-ℚ r one-ℚ r≠1))
 ```
 
 ### If `|r| < 1`, the sum of the standard geometric sequence `n ↦ arⁿ` is `a/(1-r)`
@@ -241,30 +154,24 @@ module _
           ( inv
             ( eq-htpy (compute-sum-standard-geometric-fin-sequence-ℚ a r r≠1)))
           ( equational-reasoning
-            a *ℚ
-            ( (one-ℚ -ℚ zero-ℚ) *ℚ
-              rational-inv-ℚˣ (invertible-diff-neq-ℚ r one-ℚ r≠1))
+            a *ℚ rational-inv-ℚˣ (invertible-diff-neq-ℚ r one-ℚ r≠1) *ℚ
+            (one-ℚ -ℚ zero-ℚ)
+            ＝
+              a *ℚ rational-inv-ℚˣ (invertible-diff-neq-ℚ r one-ℚ r≠1) *ℚ one-ℚ
+              by ap-mul-ℚ refl (right-zero-law-diff-ℚ _)
             ＝
-              a *ℚ
-              ( one-ℚ *ℚ rational-inv-ℚˣ (invertible-diff-neq-ℚ r one-ℚ r≠1))
-              by ap-mul-ℚ refl (ap-mul-ℚ (right-zero-law-diff-ℚ one-ℚ) refl)
-            ＝ a *ℚ rational-inv-ℚˣ (invertible-diff-neq-ℚ r one-ℚ r≠1)
-              by ap-mul-ℚ refl (left-unit-law-mul-ℚ _))
-          ( uniformly-continuous-map-limit-sequence-Metric-Space
+              a *ℚ rational-inv-ℚˣ (invertible-diff-neq-ℚ r one-ℚ r≠1)
+              by right-unit-law-mul-ℚ _)
+          ( preserves-limits-sequence-uniformly-continuous-function-Metric-Space
             ( metric-space-ℚ)
             ( metric-space-ℚ)
             ( comp-uniformly-continuous-function-Metric-Space
               ( metric-space-ℚ)
               ( metric-space-ℚ)
               ( metric-space-ℚ)
-              ( uniformly-continuous-left-mul-ℚ a)
-              ( comp-uniformly-continuous-function-Metric-Space
-                ( metric-space-ℚ)
-                ( metric-space-ℚ)
-                ( metric-space-ℚ)
-                ( uniformly-continuous-right-mul-ℚ
-                  ( rational-inv-ℚˣ (invertible-diff-neq-ℚ r one-ℚ r≠1)))
-                ( uniformly-continuous-diff-ℚ one-ℚ)))
+              ( uniformly-continuous-left-mul-ℚ
+                ( a *ℚ rational-inv-ℚˣ (invertible-diff-neq-ℚ r one-ℚ r≠1)))
+              ( uniformly-continuous-diff-ℚ one-ℚ))
             ( λ n → power-ℚ n r)
             ( zero-ℚ)
             ( is-zero-limit-power-le-one-abs-ℚ r |r|<1))
diff --git a/src/elementary-number-theory/triangular-numbers.lagda.md b/src/elementary-number-theory/triangular-numbers.lagda.md
index 23ae32125c..0a3f74aae1 100644
--- a/src/elementary-number-theory/triangular-numbers.lagda.md
+++ b/src/elementary-number-theory/triangular-numbers.lagda.md
@@ -284,7 +284,7 @@ abstract
           by ap-mul-ℚ refl (right-zero-law-diff-ℚ one-ℚ)
         ＝ rational-ℕ 2
           by right-unit-law-mul-ℚ _)
-      ( uniformly-continuous-map-limit-sequence-Metric-Space
+      ( preserves-limits-sequence-uniformly-continuous-function-Metric-Space
         ( metric-space-ℚ)
         ( metric-space-ℚ)
         ( comp-uniformly-continuous-function-Metric-Space
diff --git a/src/literature/100-theorems.lagda.md b/src/literature/100-theorems.lagda.md
index a17c9a0db8..862d0a1cea 100644
--- a/src/literature/100-theorems.lagda.md
+++ b/src/literature/100-theorems.lagda.md
@@ -116,6 +116,16 @@ open import foundation.cantors-theorem using
   ( theorem-Cantor)
 ```
 
+### 66. Sum of a Geometric Series {#66}
+
+**Author:** [Louis Wasserman](https://github.com/lowasser)
+
+```agda
+open import real-numbers.geometric-sequences-real-numbers using
+  ( compute-sum-standard-geometric-fin-sequence-ℝ ;
+    compute-sum-standard-geometric-series-ℝ)
+```
+
 ### 68. Sum of an arithmetic series {#68}
 
 **Author:** [malarbol](http://www.github.com/malarbol)
diff --git a/src/metric-spaces/cauchy-approximations-metric-quotients-of-pseudometric-spaces.lagda.md b/src/metric-spaces/cauchy-approximations-metric-quotients-of-pseudometric-spaces.lagda.md
index 13705b93b6..9184f29af6 100644
--- a/src/metric-spaces/cauchy-approximations-metric-quotients-of-pseudometric-spaces.lagda.md
+++ b/src/metric-spaces/cauchy-approximations-metric-quotients-of-pseudometric-spaces.lagda.md
@@ -206,12 +206,12 @@ module _
     is-limit-cauchy-approximation-Pseudometric-Space M u lim)
   where
 
-  preserves-limit-map-metric-quotient-cauchy-approximation-Pseudometric-Space :
+  preserves-limits-map-metric-quotient-cauchy-approximation-Pseudometric-Space :
     is-limit-cauchy-approximation-Metric-Space
       ( metric-quotient-Pseudometric-Space M)
       ( map-metric-quotient-cauchy-approximation-Pseudometric-Space M u)
       ( map-metric-quotient-Pseudometric-Space M lim)
-  preserves-limit-map-metric-quotient-cauchy-approximation-Pseudometric-Space
+  preserves-limits-map-metric-quotient-cauchy-approximation-Pseudometric-Space
     ε δ (x , x∈uε) (y , y∈lim) =
     let
       lim~y : sim-Pseudometric-Space M lim y
diff --git a/src/metric-spaces/convergent-sequences-metric-spaces.lagda.md b/src/metric-spaces/convergent-sequences-metric-spaces.lagda.md
index 073ef2f615..b2dc8712ac 100644
--- a/src/metric-spaces/convergent-sequences-metric-spaces.lagda.md
+++ b/src/metric-spaces/convergent-sequences-metric-spaces.lagda.md
@@ -111,7 +111,7 @@ module _
         ( seq-modulated-ucont-map-convergent-sequence-Metric-Space)
         ( limit-seq-modulated-ucont-map-convergent-sequence-Metric-Space)
     is-limit-seq-modulated-ucont-map-convergent-sequence-Metric-Space =
-      modulated-ucont-map-limit-sequence-Metric-Space
+      preserves-limits-sequence-modulated-ucont-map-Metric-Space
         ( A)
         ( B)
         ( f)
@@ -162,7 +162,7 @@ module _
         ( seq-uniformly-continuous-map-convergent-sequence-Metric-Space)
         ( limit-seq-uniformly-continuous-map-convergent-sequence-Metric-Space)
     is-limit-seq-uniformly-continuous-map-convergent-sequence-Metric-Space =
-      uniformly-continuous-map-limit-sequence-Metric-Space
+      preserves-limits-sequence-uniformly-continuous-function-Metric-Space
         ( A)
         ( B)
         ( f)
@@ -206,7 +206,7 @@ module _
   has-limit-seq-short-map-convergent-sequence-Metric-Space =
     ( map-short-function-Metric-Space A B f
       ( limit-convergent-sequence-Metric-Space A u)) ,
-    ( short-map-limit-sequence-Metric-Space
+    ( preserves-limits-sequence-short-function-Metric-Space
       ( A)
       ( B)
       ( f)
diff --git a/src/metric-spaces/limits-of-sequences-metric-spaces.lagda.md b/src/metric-spaces/limits-of-sequences-metric-spaces.lagda.md
index 219491a035..2cfda0f25e 100644
--- a/src/metric-spaces/limits-of-sequences-metric-spaces.lagda.md
+++ b/src/metric-spaces/limits-of-sequences-metric-spaces.lagda.md
@@ -292,7 +292,7 @@ module _
             ( n)
             ( N≤n)))
 
-    modulated-ucont-map-limit-sequence-Metric-Space :
+    preserves-limits-sequence-modulated-ucont-map-Metric-Space :
       is-limit-sequence-Metric-Space A u lim →
       is-limit-sequence-Metric-Space
         ( B)
@@ -300,7 +300,7 @@ module _
           ( map-modulated-ucont-map-Metric-Space A B f)
           ( u))
         ( map-modulated-ucont-map-Metric-Space A B f lim)
-    modulated-ucont-map-limit-sequence-Metric-Space =
+    preserves-limits-sequence-modulated-ucont-map-Metric-Space =
       map-is-inhabited modulated-ucont-map-limit-modulus-sequence-Metric-Space
 ```
 
@@ -317,7 +317,7 @@ module _
   where
 
   abstract
-    uniformly-continuous-map-limit-sequence-Metric-Space :
+    preserves-limits-sequence-uniformly-continuous-function-Metric-Space :
       is-limit-sequence-Metric-Space A u lim →
       is-limit-sequence-Metric-Space
         ( B)
@@ -325,11 +325,12 @@ module _
           ( map-uniformly-continuous-function-Metric-Space A B f)
           ( u))
         ( map-uniformly-continuous-function-Metric-Space A B f lim)
-    uniformly-continuous-map-limit-sequence-Metric-Space is-limit-lim =
+    preserves-limits-sequence-uniformly-continuous-function-Metric-Space
+      is-limit-lim =
       rec-trunc-Prop
         ( is-limit-prop-sequence-Metric-Space B _ _)
         ( λ m →
-          modulated-ucont-map-limit-sequence-Metric-Space
+          preserves-limits-sequence-modulated-ucont-map-Metric-Space
             ( A)
             ( B)
             ( map-uniformly-continuous-function-Metric-Space A B f , m)
@@ -370,7 +371,7 @@ module _
       ( u)
       ( lim)
 
-  short-map-limit-sequence-Metric-Space :
+  preserves-limits-sequence-short-function-Metric-Space :
     is-limit-sequence-Metric-Space A u lim →
     is-limit-sequence-Metric-Space
       ( B)
@@ -378,7 +379,7 @@ module _
         ( map-short-function-Metric-Space A B f)
         ( u))
       ( map-short-function-Metric-Space A B f lim)
-  short-map-limit-sequence-Metric-Space =
+  preserves-limits-sequence-short-function-Metric-Space =
     map-is-inhabited short-map-limit-modulus-sequence-Metric-Space
 ```
 
diff --git a/src/real-numbers.lagda.md b/src/real-numbers.lagda.md
index 3b84f6c0b0..c9c9de03d9 100644
--- a/src/real-numbers.lagda.md
+++ b/src/real-numbers.lagda.md
@@ -18,11 +18,13 @@ open import real-numbers.binary-minimum-real-numbers public
 open import real-numbers.cauchy-completeness-dedekind-real-numbers public
 open import real-numbers.cauchy-sequences-real-numbers public
 open import real-numbers.closed-intervals-real-numbers public
+open import real-numbers.convergent-series-real-numbers public
 open import real-numbers.dedekind-real-numbers public
 open import real-numbers.difference-real-numbers public
 open import real-numbers.distance-real-numbers public
 open import real-numbers.enclosing-closed-rational-intervals-real-numbers public
 open import real-numbers.finitely-enumerable-subsets-real-numbers public
+open import real-numbers.geometric-sequences-real-numbers public
 open import real-numbers.inequalities-addition-and-subtraction-real-numbers public
 open import real-numbers.inequality-lower-dedekind-real-numbers public
 open import real-numbers.inequality-nonnegative-real-numbers public
@@ -34,6 +36,7 @@ open import real-numbers.infima-families-real-numbers public
 open import real-numbers.inhabited-finitely-enumerable-subsets-real-numbers public
 open import real-numbers.inhabited-totally-bounded-subsets-real-numbers public
 open import real-numbers.isometry-addition-real-numbers public
+open import real-numbers.isometry-difference-real-numbers public
 open import real-numbers.isometry-negation-real-numbers public
 open import real-numbers.large-additive-group-of-real-numbers public
 open import real-numbers.large-multiplicative-monoid-of-real-numbers public
@@ -45,6 +48,7 @@ open import real-numbers.maximum-finite-families-real-numbers public
 open import real-numbers.maximum-inhabited-finitely-enumerable-subsets-real-numbers public
 open import real-numbers.maximum-lower-dedekind-real-numbers public
 open import real-numbers.maximum-upper-dedekind-real-numbers public
+open import real-numbers.metric-abelian-group-of-real-numbers public
 open import real-numbers.metric-space-of-nonnegative-real-numbers public
 open import real-numbers.metric-space-of-real-numbers public
 open import real-numbers.minimum-finite-families-real-numbers public
@@ -73,8 +77,10 @@ open import real-numbers.rational-real-numbers public
 open import real-numbers.rational-upper-dedekind-real-numbers public
 open import real-numbers.real-numbers-from-lower-dedekind-real-numbers public
 open import real-numbers.real-numbers-from-upper-dedekind-real-numbers public
+open import real-numbers.real-sequences-approximating-zero public
 open import real-numbers.saturation-inequality-nonnegative-real-numbers public
 open import real-numbers.saturation-inequality-real-numbers public
+open import real-numbers.series-real-numbers public
 open import real-numbers.short-function-binary-maximum-real-numbers public
 open import real-numbers.similarity-nonnegative-real-numbers public
 open import real-numbers.similarity-positive-real-numbers public
@@ -89,5 +95,6 @@ open import real-numbers.subsets-real-numbers public
 open import real-numbers.suprema-families-real-numbers public
 open import real-numbers.totally-bounded-subsets-real-numbers public
 open import real-numbers.transposition-addition-subtraction-cuts-dedekind-real-numbers public
+open import real-numbers.uniformly-continuous-functions-real-numbers public
 open import real-numbers.upper-dedekind-real-numbers public
 ```
diff --git a/src/real-numbers/apartness-real-numbers.lagda.md b/src/real-numbers/apartness-real-numbers.lagda.md
index 242133133b..a362297a3d 100644
--- a/src/real-numbers/apartness-real-numbers.lagda.md
+++ b/src/real-numbers/apartness-real-numbers.lagda.md
@@ -7,6 +7,8 @@ module real-numbers.apartness-real-numbers where
 <details><summary>Imports</summary>
 
 ```agda
+open import foundation.apartness-relations
+open import foundation.binary-transport
 open import foundation.disjunction
 open import foundation.empty-types
 open import foundation.function-types
@@ -18,7 +20,12 @@ open import foundation.negation
 open import foundation.propositions
 open import foundation.universe-levels
 
+open import real-numbers.absolute-value-real-numbers
+open import real-numbers.addition-real-numbers
 open import real-numbers.dedekind-real-numbers
+open import real-numbers.negation-real-numbers
+open import real-numbers.similarity-real-numbers
+open import real-numbers.strict-inequalities-addition-and-subtraction-real-numbers
 open import real-numbers.strict-inequality-real-numbers
 ```
 
@@ -42,6 +49,10 @@ module _
 
   apart-ℝ : UU (l1 ⊔ l2)
   apart-ℝ = type-Prop apart-prop-ℝ
+
+apart-le-ℝ :
+  {l1 l2 : Level} {x : ℝ l1} {y : ℝ l2} → le-ℝ x y → apart-ℝ x y
+apart-le-ℝ = inl-disjunction
 ```
 
 ## Properties
@@ -58,8 +69,8 @@ antireflexive-apart-ℝ x =
 
 ```agda
 symmetric-apart-ℝ :
-  {l1 l2 : Level} → (x : ℝ l1) (y : ℝ l2) → apart-ℝ x y → apart-ℝ y x
-symmetric-apart-ℝ x y =
+  {l1 l2 : Level} {x : ℝ l1} {y : ℝ l2} → apart-ℝ x y → apart-ℝ y x
+symmetric-apart-ℝ {x = x} {y = y} =
   elim-disjunction (apart-prop-ℝ y x) inr-disjunction inl-disjunction
 ```
 
@@ -91,7 +102,7 @@ apart-prop-Large-Apartness-Relation large-apartness-relation-ℝ =
   apart-prop-ℝ
 antirefl-Large-Apartness-Relation large-apartness-relation-ℝ =
   antireflexive-apart-ℝ
-symmetric-Large-Apartness-Relation large-apartness-relation-ℝ =
+symmetric-Large-Apartness-Relation large-apartness-relation-ℝ _ _ =
   symmetric-apart-ℝ
 cotransitive-Large-Apartness-Relation large-apartness-relation-ℝ =
   cotransitive-apart-ℝ
@@ -104,3 +115,77 @@ nonequal-apart-ℝ : {l : Level} (x y : ℝ l) → apart-ℝ x y → x ≠ y
 nonequal-apart-ℝ x y =
   nonequal-apart-Large-Apartness-Relation large-apartness-relation-ℝ
 ```
+
+### Apartness is preserved by translation
+
+```agda
+abstract
+  preserves-apart-left-add-ℝ :
+    {l1 l2 l3 : Level} (x : ℝ l1) (y : ℝ l2) (z : ℝ l3) →
+    apart-ℝ y z → apart-ℝ (x +ℝ y) (x +ℝ z)
+  preserves-apart-left-add-ℝ x y z =
+    map-disjunction
+      ( preserves-le-left-add-ℝ x y z)
+      ( preserves-le-left-add-ℝ x z y)
+
+  preserves-apart-right-add-ℝ :
+    {l1 l2 l3 : Level} (x : ℝ l1) (y : ℝ l2) (z : ℝ l3) →
+    apart-ℝ y z → apart-ℝ (y +ℝ x) (z +ℝ x)
+  preserves-apart-right-add-ℝ x y z y#z =
+    binary-tr
+      ( apart-ℝ)
+      ( commutative-add-ℝ x y)
+      ( commutative-add-ℝ x z)
+      ( preserves-apart-left-add-ℝ x y z y#z)
+```
+
+### Apartness is preserved by negation
+
+```agda
+abstract
+  preserves-apart-neg-ℝ :
+    {l1 l2 : Level} (x : ℝ l1) (y : ℝ l2) → apart-ℝ x y →
+    apart-ℝ (neg-ℝ x) (neg-ℝ y)
+  preserves-apart-neg-ℝ x y =
+    elim-disjunction
+      ( apart-prop-ℝ _ _)
+      ( inr-disjunction ∘ neg-le-ℝ)
+      ( inl-disjunction ∘ neg-le-ℝ)
+```
+
+### Apartness is preserved by similarity
+
+```agda
+abstract
+  apart-right-sim-ℝ :
+    {l1 l2 l3 : Level} (z : ℝ l1) (x : ℝ l2) (y : ℝ l3) →
+    sim-ℝ x y → apart-ℝ z x → apart-ℝ z y
+  apart-right-sim-ℝ z x y x~y =
+    map-disjunction
+      ( preserves-le-right-sim-ℝ z x y x~y)
+      ( preserves-le-left-sim-ℝ z x y x~y)
+
+  apart-left-sim-ℝ :
+    {l1 l2 l3 : Level} (z : ℝ l1) (x : ℝ l2) (y : ℝ l3) →
+    sim-ℝ x y → apart-ℝ x z → apart-ℝ y z
+  apart-left-sim-ℝ z x y x~y =
+    map-disjunction
+      ( preserves-le-left-sim-ℝ z x y x~y)
+      ( preserves-le-right-sim-ℝ z x y x~y)
+
+  apart-sim-ℝ :
+    {l1 l2 l3 l4 : Level} {x : ℝ l1} {x' : ℝ l2} {y : ℝ l3} {y' : ℝ l4} →
+    sim-ℝ x x' → sim-ℝ y y' → apart-ℝ x y → apart-ℝ x' y'
+  apart-sim-ℝ {x = x} {x' = x'} {y = y} {y' = y'} x~x' y~y' x#y =
+    apart-left-sim-ℝ
+      ( y')
+      ( x)
+      ( x')
+      ( x~x')
+      ( apart-right-sim-ℝ
+        ( x)
+        ( y)
+        ( y')
+        ( y~y')
+        ( x#y))
+```
diff --git a/src/real-numbers/convergent-series-real-numbers.lagda.md b/src/real-numbers/convergent-series-real-numbers.lagda.md
new file mode 100644
index 0000000000..9c8b3bd2db
--- /dev/null
+++ b/src/real-numbers/convergent-series-real-numbers.lagda.md
@@ -0,0 +1,40 @@
+# Convergent series of real numbers
+
+```agda
+{-# OPTIONS --lossy-unification #-}
+
+module real-numbers.convergent-series-real-numbers where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import analysis.convergent-series-metric-abelian-groups
+
+open import foundation.propositions
+open import foundation.universe-levels
+
+open import real-numbers.dedekind-real-numbers
+open import real-numbers.series-real-numbers
+```
+
+</details>
+
+## Idea
+
+A [series](real-numbers.series-real-numbers.md) of
+[real numbers](real-numbers.dedekind-real-numbers.md)
+{{#concept "converges" Disambiguation="series of real numbers" Agda=is-sum-series-ℝ}}
+to `x` if the sequence of its partial sums
+[converges](metric-spaces.limits-of-sequences-metric-spaces.md) to `x` in the
+[standard metric space of real numbers](real-numbers.metric-space-of-real-numbers.md).
+
+## Definition
+
+```agda
+is-sum-prop-series-ℝ : {l : Level} → series-ℝ l → ℝ l → Prop l
+is-sum-prop-series-ℝ = is-sum-prop-series-Metric-Ab
+
+is-sum-series-ℝ : {l : Level} → series-ℝ l → ℝ l → UU l
+is-sum-series-ℝ = is-sum-series-Metric-Ab
+```
diff --git a/src/real-numbers/distance-real-numbers.lagda.md b/src/real-numbers/distance-real-numbers.lagda.md
index 4bc37c1536..8b9f67f22b 100644
--- a/src/real-numbers/distance-real-numbers.lagda.md
+++ b/src/real-numbers/distance-real-numbers.lagda.md
@@ -295,7 +295,7 @@ abstract
         by sim-eq-ℝ (ap abs-ℝ (right-unit-law-add-ℝ (x -ℝ y)))
 ```
 
-## Distributivity laws
+### Distributivity laws
 
 ```agda
 module _
@@ -323,3 +323,39 @@ module _
         ＝ dist-ℝ (x *ℝ z) (y *ℝ z)
           by ap abs-ℝ (right-distributive-mul-diff-ℝ x y z)
 ```
+
+### Zero laws
+
+```agda
+abstract
+  right-zero-law-dist-ℝ : {l : Level} (x : ℝ l) → dist-ℝ x zero-ℝ ＝ abs-ℝ x
+  right-zero-law-dist-ℝ x = ap abs-ℝ (right-unit-law-diff-ℝ x)
+
+  left-zero-law-dist-ℝ : {l : Level} (x : ℝ l) → dist-ℝ zero-ℝ x ＝ abs-ℝ x
+  left-zero-law-dist-ℝ x = commutative-dist-ℝ zero-ℝ x ∙ right-zero-law-dist-ℝ x
+```
+
+### Distance is preserved by similarity
+
+```agda
+abstract
+  preserves-dist-left-sim-ℝ :
+    {l1 l2 l3 : Level} {z : ℝ l1} {x : ℝ l2} {y : ℝ l3} → sim-ℝ x y →
+    sim-ℝ (dist-ℝ x z) (dist-ℝ y z)
+  preserves-dist-left-sim-ℝ {z = z} {x = x} {y = y} x~y =
+    preserves-sim-abs-ℝ (preserves-sim-right-add-ℝ (neg-ℝ z) x y x~y)
+
+  preserves-dist-right-sim-ℝ :
+    {l1 l2 l3 : Level} {z : ℝ l1} {x : ℝ l2} {y : ℝ l3} → sim-ℝ x y →
+    sim-ℝ (dist-ℝ z x) (dist-ℝ z y)
+  preserves-dist-right-sim-ℝ {z = z} x~y =
+    preserves-sim-abs-ℝ (preserves-sim-diff-ℝ (refl-sim-ℝ z) x~y)
+
+  preserves-dist-sim-ℝ :
+    {l1 l2 l3 l4 : Level} {x : ℝ l1} {x' : ℝ l2} {y : ℝ l3} {y' : ℝ l4} →
+    sim-ℝ x x' → sim-ℝ y y' → sim-ℝ (dist-ℝ x y) (dist-ℝ x' y')
+  preserves-dist-sim-ℝ x~x' y~y' =
+    transitive-sim-ℝ _ _ _
+      ( preserves-dist-right-sim-ℝ y~y')
+      ( preserves-dist-left-sim-ℝ x~x')
+```
diff --git a/src/real-numbers/geometric-sequences-real-numbers.lagda.md b/src/real-numbers/geometric-sequences-real-numbers.lagda.md
new file mode 100644
index 0000000000..a868836657
--- /dev/null
+++ b/src/real-numbers/geometric-sequences-real-numbers.lagda.md
@@ -0,0 +1,248 @@
+# Geometric sequences of real numbers
+
+```agda
+{-# OPTIONS --lossy-unification #-}
+
+module real-numbers.geometric-sequences-real-numbers where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import commutative-algebra.geometric-sequences-commutative-rings
+
+open import elementary-number-theory.natural-numbers
+
+open import foundation.action-on-identifications-functions
+open import foundation.binary-transport
+open import foundation.function-extensionality
+open import foundation.identity-types
+open import foundation.transport-along-identifications
+open import foundation.universe-levels
+
+open import lists.sequences
+
+open import metric-spaces.limits-of-sequences-metric-spaces
+open import metric-spaces.uniformly-continuous-functions-metric-spaces
+
+open import real-numbers.absolute-value-real-numbers
+open import real-numbers.apartness-real-numbers
+open import real-numbers.convergent-series-real-numbers
+open import real-numbers.dedekind-real-numbers
+open import real-numbers.difference-real-numbers
+open import real-numbers.isometry-difference-real-numbers
+open import real-numbers.large-ring-of-real-numbers
+open import real-numbers.limits-sequences-real-numbers
+open import real-numbers.lipschitz-continuity-multiplication-real-numbers
+open import real-numbers.metric-space-of-real-numbers
+open import real-numbers.multiplication-real-numbers
+open import real-numbers.multiplicative-inverses-nonzero-real-numbers
+open import real-numbers.nonzero-real-numbers
+open import real-numbers.powers-real-numbers
+open import real-numbers.raising-universe-levels-real-numbers
+open import real-numbers.rational-real-numbers
+open import real-numbers.series-real-numbers
+open import real-numbers.similarity-real-numbers
+open import real-numbers.strict-inequality-real-numbers
+open import real-numbers.uniformly-continuous-functions-real-numbers
+```
+
+</details>
+
+## Idea
+
+A
+{{#concept "geometric sequence" Disambiguation="of real numbers" Agda=geometric-sequence-ℝ}}
+of [real numbers](real-numbers.dedekind-real-numbers.md) is a
+[geometric sequence](commutative-algebra.geometric-sequences-commutative-rings.md)
+in the
+[commutative ring of real numbers](real-numbers.large-ring-of-real-numbers.md).
+
+## Definitions
+
+```agda
+geometric-sequence-ℝ : (l : Level) → UU (lsuc l)
+geometric-sequence-ℝ l =
+  geometric-sequence-Commutative-Ring (commutative-ring-ℝ l)
+
+seq-geometric-sequence-ℝ : {l : Level} → geometric-sequence-ℝ l → sequence (ℝ l)
+seq-geometric-sequence-ℝ {l} =
+  seq-geometric-sequence-Commutative-Ring (commutative-ring-ℝ l)
+
+standard-geometric-sequence-ℝ :
+  {l : Level} → ℝ l → ℝ l → geometric-sequence-ℝ l
+standard-geometric-sequence-ℝ {l} =
+  standard-geometric-sequence-Commutative-Ring (commutative-ring-ℝ l)
+
+seq-standard-geometric-sequence-ℝ :
+  {l : Level} → ℝ l → ℝ l → sequence (ℝ l)
+seq-standard-geometric-sequence-ℝ {l} =
+  seq-standard-geometric-sequence-Commutative-Ring (commutative-ring-ℝ l)
+```
+
+## Properties
+
+### The nth term of a geometric sequence with initial term `a` and common ratio `r` is `a * rⁿ`
+
+```agda
+module _
+  {l : Level} (a r : ℝ l)
+  where
+
+  compute-standard-geometric-sequence-ℝ :
+    (n : ℕ) → seq-standard-geometric-sequence-ℝ a r n ＝ a *ℝ power-ℝ n r
+  compute-standard-geometric-sequence-ℝ n =
+    inv
+      ( htpy-mul-pow-standard-geometric-sequence-Commutative-Ring
+        ( commutative-ring-ℝ l)
+        ( a)
+        ( r)
+        ( n))
+```
+
+### If `r` is apart from `1`, the sum of the first `n` elements of the standard geometric sequence `n ↦ arⁿ` is `a(1-rⁿ)/(1-r)`
+
+```agda
+sum-standard-geometric-fin-sequence-ℝ : {l : Level} → ℝ l → ℝ l → ℕ → ℝ l
+sum-standard-geometric-fin-sequence-ℝ {l} =
+  sum-standard-geometric-fin-sequence-Commutative-Ring (commutative-ring-ℝ l)
+
+module _
+  {l : Level} (a r : ℝ l) (r≠1 : apart-ℝ r one-ℝ)
+  where
+
+  abstract
+    compute-sum-standard-geometric-fin-sequence-ℝ :
+      (n : ℕ) →
+      sum-standard-geometric-fin-sequence-ℝ a r n ＝
+      ( ( a *ℝ
+          real-inv-nonzero-ℝ
+            ( nonzero-diff-apart-ℝ one-ℝ r (symmetric-apart-ℝ r≠1))) *ℝ
+        (one-ℝ -ℝ power-ℝ n r))
+    compute-sum-standard-geometric-fin-sequence-ℝ n =
+      let
+        1#r = symmetric-apart-ℝ r≠1
+        1l#r =
+          apart-left-sim-ℝ
+            ( r)
+            ( one-ℝ)
+            ( raise-ℝ l one-ℝ)
+            ( sim-raise-ℝ l one-ℝ)
+            ( 1#r)
+      in
+        equational-reasoning
+          sum-standard-geometric-fin-sequence-ℝ a r n
+          ＝
+            ( a *ℝ
+              real-inv-nonzero-ℝ
+                ( nonzero-diff-apart-ℝ (raise-ℝ l one-ℝ) r 1l#r)) *ℝ
+            ( raise-ℝ l one-ℝ -ℝ power-ℝ n r)
+            by
+              compute-sum-standard-geometric-fin-sequence-Commutative-Ring
+                ( commutative-ring-ℝ l)
+                ( a)
+                ( r)
+                ( is-invertible-is-nonzero-ℝ _
+                  ( is-nonzero-diff-is-apart-ℝ _ _ 1l#r))
+                ( n)
+          ＝
+            ( a *ℝ real-inv-nonzero-ℝ (nonzero-diff-apart-ℝ one-ℝ r 1#r)) *ℝ
+            ( one-ℝ -ℝ power-ℝ n r)
+            by
+              ap-mul-ℝ
+                ( ap-mul-ℝ
+                  ( refl)
+                  ( ap
+                    ( real-inv-nonzero-ℝ)
+                    ( eq-nonzero-ℝ _ _
+                      ( eq-sim-ℝ
+                        ( preserves-sim-diff-ℝ
+                          ( symmetric-sim-ℝ (sim-raise-ℝ l one-ℝ))
+                          ( refl-sim-ℝ r))))))
+                ( eq-sim-ℝ
+                  ( preserves-sim-diff-ℝ
+                    ( symmetric-sim-ℝ (sim-raise-ℝ l one-ℝ))
+                    ( refl-sim-ℝ (power-ℝ n r))))
+```
+
+### If `|r| < 1`, then the geometric series `Σₙ arⁿ` converges to `a/(1-r)`
+
+This is the [66th](literature.100-theorems.md#66) theorem on
+[Freek Wiedijk](http://www.cs.ru.nl/F.Wiedijk/)'s list of
+[100 theorems](literature.100-theorems.md) {{#cite 100theorems}}.
+
+```agda
+module _
+  {l : Level} (a r : ℝ l)
+  where
+
+  standard-geometric-series-ℝ : series-ℝ l
+  standard-geometric-series-ℝ =
+    series-terms-ℝ (seq-standard-geometric-sequence-ℝ a r)
+
+  abstract
+    compute-sum-standard-geometric-series-ℝ :
+      (|r|<1 : le-ℝ (abs-ℝ r) one-ℝ) →
+      is-sum-series-ℝ
+        ( standard-geometric-series-ℝ)
+        ( a *ℝ real-inv-nonzero-ℝ (nonzero-diff-le-abs-ℝ |r|<1))
+    compute-sum-standard-geometric-series-ℝ |r|<1 =
+      let
+        r#1 = apart-le-ℝ (concatenate-leq-le-ℝ _ _ _ (leq-abs-ℝ r) |r|<1)
+      in
+        binary-tr
+          ( is-limit-sequence-ℝ)
+          ( inv
+            ( eq-htpy
+              ( λ n →
+                equational-reasoning
+                  sum-standard-geometric-fin-sequence-ℝ a r n
+                  ＝
+                    ( a *ℝ real-inv-nonzero-ℝ _) *ℝ
+                    ( one-ℝ -ℝ power-ℝ n r)
+                    by compute-sum-standard-geometric-fin-sequence-ℝ a r r#1 n
+                  ＝
+                    ( a *ℝ real-inv-nonzero-ℝ (nonzero-diff-le-abs-ℝ |r|<1)) *ℝ
+                    ( one-ℝ -ℝ power-ℝ n r)
+                    by
+                      ap
+                        ( λ z →
+                          (a *ℝ real-inv-nonzero-ℝ z) *ℝ (one-ℝ -ℝ power-ℝ n r))
+                        ( eq-nonzero-ℝ
+                          ( nonzero-diff-apart-ℝ
+                            ( one-ℝ)
+                            ( r)
+                            ( symmetric-apart-ℝ r#1))
+                          ( nonzero-diff-le-abs-ℝ |r|<1)
+                          ( refl)))))
+          ( equational-reasoning
+            ( a *ℝ real-inv-nonzero-ℝ (nonzero-diff-le-abs-ℝ |r|<1)) *ℝ
+            ( one-ℝ -ℝ raise-ℝ l zero-ℝ)
+            ＝
+              ( a *ℝ real-inv-nonzero-ℝ (nonzero-diff-le-abs-ℝ |r|<1)) *ℝ
+              ( one-ℝ -ℝ zero-ℝ)
+              by
+                eq-sim-ℝ
+                  ( preserves-sim-left-mul-ℝ _ _ _
+                    ( preserves-sim-diff-ℝ
+                      ( refl-sim-ℝ one-ℝ)
+                      ( symmetric-sim-ℝ (sim-raise-ℝ l zero-ℝ))))
+            ＝
+              ( a *ℝ real-inv-nonzero-ℝ (nonzero-diff-le-abs-ℝ |r|<1)) *ℝ one-ℝ
+              by ap-mul-ℝ refl (right-unit-law-diff-ℝ one-ℝ)
+            ＝ a *ℝ real-inv-nonzero-ℝ (nonzero-diff-le-abs-ℝ |r|<1)
+              by right-unit-law-mul-ℝ _)
+          ( preserves-limits-sequence-uniformly-continuous-function-ℝ
+            ( comp-uniformly-continuous-function-ℝ
+              ( uniformly-continuous-right-mul-ℝ
+                ( l)
+                ( a *ℝ real-inv-nonzero-ℝ (nonzero-diff-le-abs-ℝ |r|<1)))
+              ( uniformly-continuous-diff-ℝ one-ℝ))
+            ( λ n → power-ℝ n r)
+            ( raise-ℝ l zero-ℝ)
+            ( is-zero-lim-power-le-one-abs-ℝ r |r|<1))
+```
+
+## References
+
+{{#bibliography}}
diff --git a/src/real-numbers/isometry-difference-real-numbers.lagda.md b/src/real-numbers/isometry-difference-real-numbers.lagda.md
new file mode 100644
index 0000000000..73b411df6a
--- /dev/null
+++ b/src/real-numbers/isometry-difference-real-numbers.lagda.md
@@ -0,0 +1,73 @@
+# The difference isometry on real numbers
+
+```agda
+{-# OPTIONS --lossy-unification #-}
+
+module real-numbers.isometry-difference-real-numbers where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.dependent-pair-types
+open import foundation.universe-levels
+
+open import metric-spaces.isometries-metric-spaces
+open import metric-spaces.uniformly-continuous-functions-metric-spaces
+
+open import real-numbers.addition-real-numbers
+open import real-numbers.dedekind-real-numbers
+open import real-numbers.difference-real-numbers
+open import real-numbers.isometry-addition-real-numbers
+open import real-numbers.isometry-negation-real-numbers
+open import real-numbers.metric-space-of-real-numbers
+open import real-numbers.negation-real-numbers
+```
+
+</details>
+
+## Idea
+
+[Subtracting](real-numbers.difference-real-numbers.md) from a fixed
+[real number](real-numbers.dedekind-real-numbers.md) is an
+[isometry](metric-spaces.isometries-metric-spaces.md) from the
+[metric space of real numbers](real-numbers.metric-space-of-real-numbers.md) to
+itself.
+
+## Definition
+
+```agda
+module _
+  {l1 l2 : Level} (x : ℝ l1)
+  where
+
+  abstract
+    is-isometry-diff-ℝ :
+      is-isometry-Metric-Space
+        ( metric-space-ℝ l2)
+        ( metric-space-ℝ (l1 ⊔ l2))
+        ( diff-ℝ x)
+    is-isometry-diff-ℝ =
+      is-isometry-comp-is-isometry-Metric-Space
+        ( metric-space-ℝ l2)
+        ( metric-space-ℝ l2)
+        ( metric-space-ℝ (l1 ⊔ l2))
+        ( add-ℝ x)
+        ( neg-ℝ)
+        ( is-isometry-left-add-ℝ x)
+        ( is-isometry-neg-ℝ)
+
+  isometry-diff-ℝ :
+    isometry-Metric-Space (metric-space-ℝ l2) (metric-space-ℝ (l1 ⊔ l2))
+  isometry-diff-ℝ = (diff-ℝ x , is-isometry-diff-ℝ)
+
+  uniformly-continuous-diff-ℝ :
+    uniformly-continuous-function-Metric-Space
+      ( metric-space-ℝ l2)
+      ( metric-space-ℝ (l1 ⊔ l2))
+  uniformly-continuous-diff-ℝ =
+    uniformly-continuous-isometry-Metric-Space
+      ( metric-space-ℝ l2)
+      ( metric-space-ℝ (l1 ⊔ l2))
+      ( isometry-diff-ℝ)
+```
diff --git a/src/real-numbers/large-multiplicative-monoid-of-real-numbers.lagda.md b/src/real-numbers/large-multiplicative-monoid-of-real-numbers.lagda.md
index b5d2a73c59..b3829c7449 100644
--- a/src/real-numbers/large-multiplicative-monoid-of-real-numbers.lagda.md
+++ b/src/real-numbers/large-multiplicative-monoid-of-real-numbers.lagda.md
@@ -48,7 +48,7 @@ large-monoid-mul-ℝ =
     ( large-similarity-relation-sim-ℝ)
     ( raise-ℝ)
     ( sim-raise-ℝ)
-    ( preserves-sim-mul-ℝ)
+    ( λ _ _ x~x' _ _ y~y' → preserves-sim-mul-ℝ x~x' y~y')
     ( one-ℝ)
     ( left-unit-law-mul-ℝ)
     ( right-unit-law-mul-ℝ)
diff --git a/src/real-numbers/large-ring-of-real-numbers.lagda.md b/src/real-numbers/large-ring-of-real-numbers.lagda.md
index 98fd1e8782..d1d3b2b5ee 100644
--- a/src/real-numbers/large-ring-of-real-numbers.lagda.md
+++ b/src/real-numbers/large-ring-of-real-numbers.lagda.md
@@ -44,7 +44,7 @@ large-ring-ℝ =
   make-Large-Ring
     ( large-ab-add-ℝ)
     ( mul-ℝ)
-    ( preserves-sim-mul-ℝ)
+    ( λ _ _ a~a' _ _ → preserves-sim-mul-ℝ a~a')
     ( one-ℝ)
     ( associative-mul-ℝ)
     ( left-unit-law-mul-ℝ)
diff --git a/src/real-numbers/limits-sequences-real-numbers.lagda.md b/src/real-numbers/limits-sequences-real-numbers.lagda.md
index f7ab605183..4636b60dcd 100644
--- a/src/real-numbers/limits-sequences-real-numbers.lagda.md
+++ b/src/real-numbers/limits-sequences-real-numbers.lagda.md
@@ -10,6 +10,8 @@ module real-numbers.limits-sequences-real-numbers where
 
 ```agda
 open import foundation.dependent-pair-types
+open import foundation.propositional-truncations
+open import foundation.propositions
 open import foundation.universe-levels
 
 open import lists.sequences
@@ -21,6 +23,7 @@ open import real-numbers.addition-real-numbers
 open import real-numbers.dedekind-real-numbers
 open import real-numbers.isometry-addition-real-numbers
 open import real-numbers.metric-space-of-real-numbers
+open import real-numbers.uniformly-continuous-functions-real-numbers
 ```
 
 </details>
@@ -34,6 +37,10 @@ On this page, we describe properties of
 ## Definition
 
 ```agda
+is-limit-prop-sequence-ℝ : {l : Level} → sequence (ℝ l) → ℝ l → Prop l
+is-limit-prop-sequence-ℝ {l} =
+  is-limit-prop-sequence-Metric-Space (metric-space-ℝ l)
+
 is-limit-sequence-ℝ : {l : Level} → sequence (ℝ l) → ℝ l → UU l
 is-limit-sequence-ℝ {l} = is-limit-sequence-Metric-Space (metric-space-ℝ l)
 ```
@@ -54,13 +61,13 @@ module _
   where
 
   abstract
-    is-limit-add-sequence-ℝ :
+    preserves-limits-add-sequence-ℝ :
       is-limit-sequence-Metric-Space
         ( metric-space-ℝ (l1 ⊔ l2))
         ( binary-map-sequence add-ℝ u v)
         ( lim-u +ℝ lim-v)
-    is-limit-add-sequence-ℝ =
-      modulated-ucont-map-limit-sequence-Metric-Space
+    preserves-limits-add-sequence-ℝ =
+      preserves-limits-sequence-modulated-ucont-map-Metric-Space
         ( product-Metric-Space (metric-space-ℝ l1) (metric-space-ℝ l2))
         ( metric-space-ℝ (l1 ⊔ l2))
         ( modulated-ucont-add-pair-ℝ l1 l2)
@@ -72,3 +79,30 @@ module _
           ( Hu)
           ( Hv))
 ```
+
+### Uniformly continuous functions from `ℝ` to `ℝ` preserve limits
+
+```agda
+module _
+  {l1 l2 : Level}
+  (f : uniformly-continuous-function-ℝ l1 l2)
+  (u : sequence (ℝ l1))
+  (lim : ℝ l1)
+  where
+
+  abstract
+    preserves-limits-sequence-uniformly-continuous-function-ℝ :
+      is-limit-sequence-ℝ u lim →
+      is-limit-sequence-ℝ
+        ( map-sequence
+          ( map-uniformly-continuous-function-ℝ f)
+          ( u))
+        ( map-uniformly-continuous-function-ℝ f lim)
+    preserves-limits-sequence-uniformly-continuous-function-ℝ =
+      preserves-limits-sequence-uniformly-continuous-function-Metric-Space
+        ( metric-space-ℝ l1)
+        ( metric-space-ℝ l2)
+        ( f)
+        ( u)
+        ( lim)
+```
diff --git a/src/real-numbers/lipschitz-continuity-multiplication-real-numbers.lagda.md b/src/real-numbers/lipschitz-continuity-multiplication-real-numbers.lagda.md
index b44914841b..7e881fca25 100644
--- a/src/real-numbers/lipschitz-continuity-multiplication-real-numbers.lagda.md
+++ b/src/real-numbers/lipschitz-continuity-multiplication-real-numbers.lagda.md
@@ -38,6 +38,7 @@ open import real-numbers.multiplication-real-numbers
 open import real-numbers.nonnegative-real-numbers
 open import real-numbers.rational-real-numbers
 open import real-numbers.strict-inequality-real-numbers
+open import real-numbers.uniformly-continuous-functions-real-numbers
 ```
 
 </details>
@@ -148,16 +149,12 @@ module _
         ( is-lipschitz-left-mul-ℝ l2 c)
 
   uniformly-continuous-right-mul-ℝ :
-    uniformly-continuous-function-Metric-Space
-      ( metric-space-ℝ l2)
-      ( metric-space-ℝ (l1 ⊔ l2))
+    uniformly-continuous-function-ℝ l2 (l1 ⊔ l2)
   uniformly-continuous-right-mul-ℝ =
     ( mul-ℝ c , is-uniformly-continuous-right-mul-ℝ)
 
   uniformly-continuous-left-mul-ℝ :
-    uniformly-continuous-function-Metric-Space
-      ( metric-space-ℝ l2)
-      ( metric-space-ℝ (l1 ⊔ l2))
+    uniformly-continuous-function-ℝ l2 (l1 ⊔ l2)
   uniformly-continuous-left-mul-ℝ =
     ( mul-ℝ' c , is-uniformly-continuous-left-mul-ℝ)
 ```
diff --git a/src/real-numbers/metric-abelian-group-of-real-numbers.lagda.md b/src/real-numbers/metric-abelian-group-of-real-numbers.lagda.md
new file mode 100644
index 0000000000..3402489495
--- /dev/null
+++ b/src/real-numbers/metric-abelian-group-of-real-numbers.lagda.md
@@ -0,0 +1,44 @@
+# The metric abelian group of real numbers
+
+```agda
+{-# OPTIONS --lossy-unification #-}
+
+module real-numbers.metric-abelian-group-of-real-numbers where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import analysis.metric-abelian-groups
+
+open import foundation.dependent-pair-types
+open import foundation.universe-levels
+
+open import metric-spaces.pseudometric-spaces
+
+open import real-numbers.isometry-addition-real-numbers
+open import real-numbers.isometry-negation-real-numbers
+open import real-numbers.large-additive-group-of-real-numbers
+open import real-numbers.metric-space-of-real-numbers
+```
+
+</details>
+
+## Idea
+
+The [Dedekind real numbers](real-numbers.dedekind-real-numbers.md) form a
+[metric abelian group](analysis.metric-abelian-groups.md) under
+[addition](real-numbers.addition-real-numbers.md) with regards to their
+[standard metric space](real-numbers.metric-space-of-real-numbers.md).
+
+## Definition
+
+```agda
+metric-ab-ℝ : (l : Level) → Metric-Ab (lsuc l) l
+metric-ab-ℝ l =
+  ( ab-add-ℝ l ,
+    structure-Pseudometric-Space (pseudometric-space-ℝ l) ,
+    is-extensional-pseudometric-space-ℝ ,
+    is-isometry-neg-ℝ ,
+    is-isometry-left-add-ℝ)
+```
diff --git a/src/real-numbers/multiplication-real-numbers.lagda.md b/src/real-numbers/multiplication-real-numbers.lagda.md
index 22733658d6..e228164d2d 100644
--- a/src/real-numbers/multiplication-real-numbers.lagda.md
+++ b/src/real-numbers/multiplication-real-numbers.lagda.md
@@ -1150,10 +1150,10 @@ module _
 abstract
   preserves-sim-mul-ℝ :
     {l1 l2 l3 l4 : Level} →
-    (a : ℝ l1) (a' : ℝ l2) → sim-ℝ a a' →
-    (b : ℝ l3) (b' : ℝ l4) → sim-ℝ b b' →
+    {a : ℝ l1} {a' : ℝ l2} → sim-ℝ a a' →
+    {b : ℝ l3} {b' : ℝ l4} → sim-ℝ b b' →
     sim-ℝ (a *ℝ b) (a' *ℝ b')
-  preserves-sim-mul-ℝ a a' a~a' b b' b~b' =
+  preserves-sim-mul-ℝ {a = a} {a' = a'} a~a' {b = b} {b' = b'} b~b' =
     transitive-sim-ℝ
       ( a *ℝ b)
       ( a *ℝ b')
diff --git a/src/real-numbers/multiplicative-inverses-nonzero-real-numbers.lagda.md b/src/real-numbers/multiplicative-inverses-nonzero-real-numbers.lagda.md
index 51ab87da43..aedb75f632 100644
--- a/src/real-numbers/multiplicative-inverses-nonzero-real-numbers.lagda.md
+++ b/src/real-numbers/multiplicative-inverses-nonzero-real-numbers.lagda.md
@@ -9,6 +9,8 @@ module real-numbers.multiplicative-inverses-nonzero-real-numbers where
 <details><summary>Imports</summary>
 
 ```agda
+open import commutative-algebra.invertible-elements-commutative-rings
+
 open import elementary-number-theory.inequality-rational-numbers
 open import elementary-number-theory.minimum-rational-numbers
 open import elementary-number-theory.multiplication-closed-intervals-rational-numbers
@@ -32,12 +34,15 @@ open import foundation.transport-along-identifications
 open import foundation.universe-levels
 
 open import real-numbers.dedekind-real-numbers
+open import real-numbers.inequality-real-numbers
+open import real-numbers.large-ring-of-real-numbers
 open import real-numbers.multiplication-real-numbers
 open import real-numbers.multiplicative-inverses-negative-real-numbers
 open import real-numbers.multiplicative-inverses-positive-real-numbers
 open import real-numbers.negative-real-numbers
 open import real-numbers.nonzero-real-numbers
 open import real-numbers.positive-real-numbers
+open import real-numbers.raising-universe-levels-real-numbers
 open import real-numbers.rational-real-numbers
 open import real-numbers.similarity-real-numbers
 ```
@@ -120,13 +125,27 @@ module _
   right-inverse-law-mul-nonzero-ℝ = pr2 has-nonzero-inv-nonzero-ℝ
 
   abstract
-    left-inverse-law-nonzero-ℝ :
+    left-inverse-law-mul-nonzero-ℝ :
       sim-ℝ (real-inv-nonzero-ℝ *ℝ real-nonzero-ℝ x) one-ℝ
-    left-inverse-law-nonzero-ℝ =
+    left-inverse-law-mul-nonzero-ℝ =
       tr
         ( λ y → sim-ℝ y one-ℝ)
         ( commutative-mul-ℝ _ _)
         ( right-inverse-law-mul-nonzero-ℝ)
+
+is-invertible-is-nonzero-ℝ :
+  {l : Level} (x : ℝ l) → is-nonzero-ℝ x →
+  is-invertible-element-Commutative-Ring (commutative-ring-ℝ l) x
+is-invertible-is-nonzero-ℝ x x≠0 =
+  ( real-inv-nonzero-ℝ (x , x≠0) ,
+    eq-sim-ℝ
+      ( transitive-sim-ℝ _ _ _
+        ( sim-raise-ℝ _ _)
+        ( right-inverse-law-mul-nonzero-ℝ (x , x≠0))) ,
+    eq-sim-ℝ
+      ( transitive-sim-ℝ _ _ _
+        ( sim-raise-ℝ _ _)
+        ( left-inverse-law-mul-nonzero-ℝ (x , x≠0))))
 ```
 
 ### If a real number has a multiplicative inverse, it is nonzero
@@ -225,3 +244,24 @@ abstract
     unique-right-inv-nonzero-ℝ y x
       ( tr (λ z → sim-ℝ z one-ℝ) (commutative-mul-ℝ _ _) xy=1)
 ```
+
+### If two nonzero real numbers are similar, so are their inverses
+
+```agda
+abstract
+  preserves-sim-inv-nonzero-ℝ :
+    {l1 l2 : Level} (x : nonzero-ℝ l1) (y : nonzero-ℝ l2) →
+    sim-ℝ (real-nonzero-ℝ x) (real-nonzero-ℝ y) →
+    sim-ℝ (real-inv-nonzero-ℝ x) (real-inv-nonzero-ℝ y)
+  preserves-sim-inv-nonzero-ℝ (x , x≠0) (y , y≠0) x~y =
+    symmetric-sim-ℝ
+      ( unique-right-inv-nonzero-ℝ
+        ( x , x≠0)
+        ( inv-nonzero-ℝ (y , y≠0))
+        ( similarity-reasoning-ℝ
+          x *ℝ real-inv-nonzero-ℝ (y , y≠0)
+          ~ℝ y *ℝ real-inv-nonzero-ℝ (y , y≠0)
+            by preserves-sim-right-mul-ℝ _ _ _ x~y
+          ~ℝ one-ℝ
+            by right-inverse-law-mul-nonzero-ℝ (y , y≠0)))
+```
diff --git a/src/real-numbers/nonnegative-real-numbers.lagda.md b/src/real-numbers/nonnegative-real-numbers.lagda.md
index c7b56ff0af..d536334e57 100644
--- a/src/real-numbers/nonnegative-real-numbers.lagda.md
+++ b/src/real-numbers/nonnegative-real-numbers.lagda.md
@@ -36,7 +36,9 @@ open import real-numbers.dedekind-real-numbers
 open import real-numbers.difference-real-numbers
 open import real-numbers.inequalities-addition-and-subtraction-real-numbers
 open import real-numbers.inequality-real-numbers
+open import real-numbers.raising-universe-levels-real-numbers
 open import real-numbers.rational-real-numbers
+open import real-numbers.similarity-real-numbers
 open import real-numbers.strict-inequality-real-numbers
 ```
 
@@ -126,6 +128,11 @@ abstract
   preserves-is-nonnegative-real-ℚ is-nonneg-q =
     preserves-leq-real-ℚ (leq-zero-is-nonnegative-ℚ is-nonneg-q)
 
+  reflects-is-nonnegative-real-ℚ :
+    {q : ℚ} → is-nonnegative-ℝ (real-ℚ q) → is-nonnegative-ℚ q
+  reflects-is-nonnegative-real-ℚ 0≤qℝ =
+    is-nonnegative-leq-zero-ℚ (reflects-leq-real-ℚ 0≤qℝ)
+
 nonnegative-real-ℚ⁰⁺ : ℚ⁰⁺ → ℝ⁰⁺ lzero
 nonnegative-real-ℚ⁰⁺ (q , is-nonneg-q) =
   ( real-ℚ q , preserves-is-nonnegative-real-ℚ is-nonneg-q)
@@ -277,4 +284,29 @@ abstract
     {l1 l2 : Level} (x : ℝ⁰⁺ l1) (y : ℝ l2) → leq-ℝ (real-ℝ⁰⁺ x) y →
     is-nonnegative-ℝ y
   is-nonnegative-leq-ℝ⁰⁺ (x , 0≤x) y x≤y = transitive-leq-ℝ zero-ℝ x y x≤y 0≤x
+
+  is-nonnegative-le-ℝ⁰⁺ :
+    {l1 l2 : Level} (x : ℝ⁰⁺ l1) (y : ℝ l2) → le-ℝ (real-ℝ⁰⁺ x) y →
+    is-nonnegative-ℝ y
+  is-nonnegative-le-ℝ⁰⁺ x y x<y =
+    is-nonnegative-leq-ℝ⁰⁺ x y (leq-le-ℝ x<y)
+```
+
+### Nonnegativity is preserved by similarity
+
+```agda
+abstract
+  is-nonnegative-sim-ℝ :
+    {l1 l2 : Level} {x : ℝ l1} {y : ℝ l2} → is-nonnegative-ℝ x → sim-ℝ x y →
+    is-nonnegative-ℝ y
+  is-nonnegative-sim-ℝ {x = x} {y = y} 0≤x x~y =
+    preserves-leq-right-sim-ℝ x~y 0≤x
+```
+
+### Raising the universe levels of nonnegative real numbers
+
+```agda
+raise-ℝ⁰⁺ : {l1 : Level} (l : Level) → ℝ⁰⁺ l1 → ℝ⁰⁺ (l ⊔ l1)
+raise-ℝ⁰⁺ l (x , is-nonneg-x) =
+  (raise-ℝ l x , is-nonnegative-sim-ℝ is-nonneg-x (sim-raise-ℝ l x))
 ```
diff --git a/src/real-numbers/nonzero-real-numbers.lagda.md b/src/real-numbers/nonzero-real-numbers.lagda.md
index 50018c445b..c628c950a6 100644
--- a/src/real-numbers/nonzero-real-numbers.lagda.md
+++ b/src/real-numbers/nonzero-real-numbers.lagda.md
@@ -14,13 +14,20 @@ open import foundation.disjunction
 open import foundation.identity-types
 open import foundation.propositions
 open import foundation.subtypes
+open import foundation.transport-along-identifications
 open import foundation.universe-levels
 
+open import real-numbers.absolute-value-real-numbers
+open import real-numbers.addition-real-numbers
 open import real-numbers.apartness-real-numbers
 open import real-numbers.dedekind-real-numbers
+open import real-numbers.difference-real-numbers
+open import real-numbers.negation-real-numbers
 open import real-numbers.negative-real-numbers
 open import real-numbers.positive-real-numbers
 open import real-numbers.rational-real-numbers
+open import real-numbers.similarity-real-numbers
+open import real-numbers.strict-inequality-real-numbers
 ```
 
 </details>
@@ -86,3 +93,48 @@ eq-nonzero-ℝ :
   x ＝ y
 eq-nonzero-ℝ _ _ = eq-type-subtype is-nonzero-prop-ℝ
 ```
+
+### Two real numbers are apart if and only if their difference is nonzero
+
+```agda
+module _
+  {l1 l2 : Level} (x : ℝ l1) (y : ℝ l2)
+  where
+
+  abstract
+    is-nonzero-diff-is-apart-ℝ : apart-ℝ x y → is-nonzero-ℝ (x -ℝ y)
+    is-nonzero-diff-is-apart-ℝ x#y =
+      apart-right-sim-ℝ
+        ( x -ℝ y)
+        ( y -ℝ y)
+        ( zero-ℝ)
+        ( right-inverse-law-add-ℝ y)
+        ( preserves-apart-right-add-ℝ (neg-ℝ y) x y x#y)
+
+    is-apart-is-nonzero-diff-ℝ : is-nonzero-ℝ (x -ℝ y) → apart-ℝ x y
+    is-apart-is-nonzero-diff-ℝ x-y#0 =
+      apart-sim-ℝ
+        ( cancel-right-diff-add-ℝ x y)
+        ( sim-eq-ℝ (left-unit-law-add-ℝ y))
+        ( preserves-apart-right-add-ℝ y _ _ x-y#0)
+
+  nonzero-diff-apart-ℝ : apart-ℝ x y → nonzero-ℝ (l1 ⊔ l2)
+  nonzero-diff-apart-ℝ x#y = (x -ℝ y , is-nonzero-diff-is-apart-ℝ x#y)
+```
+
+### The nonzero difference of a pair of real numbers `x` and `y` such that `x < y`
+
+```agda
+nonzero-diff-le-ℝ :
+  {l1 l2 : Level} {x : ℝ l1} {y : ℝ l2} → le-ℝ x y → nonzero-ℝ (l1 ⊔ l2)
+nonzero-diff-le-ℝ {x = x} {y = y} x<y = nonzero-ℝ⁺ (positive-diff-le-ℝ x<y)
+```
+
+### The nonzero difference of a pair of real numbers `x` and `y` such that `|x| < y`
+
+```agda
+nonzero-diff-le-abs-ℝ :
+  {l1 l2 : Level} {x : ℝ l1} {y : ℝ l2} → le-ℝ (abs-ℝ x) y → nonzero-ℝ (l1 ⊔ l2)
+nonzero-diff-le-abs-ℝ {x = x} {y = y} |x|<y =
+  nonzero-diff-le-ℝ (concatenate-leq-le-ℝ x (abs-ℝ x) y (leq-abs-ℝ x) |x|<y)
+```
diff --git a/src/real-numbers/positive-and-negative-real-numbers.lagda.md b/src/real-numbers/positive-and-negative-real-numbers.lagda.md
index d1d0920e34..18f7f33b89 100644
--- a/src/real-numbers/positive-and-negative-real-numbers.lagda.md
+++ b/src/real-numbers/positive-and-negative-real-numbers.lagda.md
@@ -86,10 +86,4 @@ abstract
     {l1 l2 : Level} (x : ℝ⁰⁺ l1) (y : ℝ l2) → le-ℝ (real-ℝ⁰⁺ x) y →
     is-positive-ℝ y
   is-positive-le-ℝ⁰⁺ (x , 0≤x) y = concatenate-leq-le-ℝ zero-ℝ x y 0≤x
-
-  is-nonnegative-le-ℝ⁰⁺ :
-    {l1 l2 : Level} (x : ℝ⁰⁺ l1) (y : ℝ l2) → le-ℝ (real-ℝ⁰⁺ x) y →
-    is-nonnegative-ℝ y
-  is-nonnegative-le-ℝ⁰⁺ x y x<y =
-    is-nonnegative-is-positive-ℝ (is-positive-le-ℝ⁰⁺ x y x<y)
 ```
diff --git a/src/real-numbers/powers-real-numbers.lagda.md b/src/real-numbers/powers-real-numbers.lagda.md
index 55ff07d63d..67caeae578 100644
--- a/src/real-numbers/powers-real-numbers.lagda.md
+++ b/src/real-numbers/powers-real-numbers.lagda.md
@@ -16,6 +16,8 @@ open import elementary-number-theory.addition-natural-numbers
 open import elementary-number-theory.multiplication-natural-numbers
 open import elementary-number-theory.natural-numbers
 open import elementary-number-theory.parity-natural-numbers
+open import elementary-number-theory.positive-rational-numbers
+open import elementary-number-theory.powers-positive-rational-numbers
 open import elementary-number-theory.powers-rational-numbers
 open import elementary-number-theory.rational-numbers
 open import elementary-number-theory.ring-of-rational-numbers
@@ -23,6 +25,7 @@ open import elementary-number-theory.ring-of-rational-numbers
 open import foundation.action-on-identifications-functions
 open import foundation.dependent-pair-types
 open import foundation.identity-types
+open import foundation.propositional-truncations
 open import foundation.transport-along-identifications
 open import foundation.universe-levels
 
@@ -30,6 +33,7 @@ open import order-theory.large-posets
 
 open import real-numbers.absolute-value-real-numbers
 open import real-numbers.dedekind-real-numbers
+open import real-numbers.inequality-nonnegative-real-numbers
 open import real-numbers.inequality-real-numbers
 open import real-numbers.large-ring-of-real-numbers
 open import real-numbers.multiplication-nonnegative-real-numbers
@@ -39,11 +43,14 @@ open import real-numbers.multiplication-real-numbers
 open import real-numbers.negation-real-numbers
 open import real-numbers.negative-real-numbers
 open import real-numbers.nonnegative-real-numbers
+open import real-numbers.positive-and-negative-real-numbers
 open import real-numbers.positive-real-numbers
 open import real-numbers.raising-universe-levels-real-numbers
 open import real-numbers.rational-real-numbers
+open import real-numbers.real-sequences-approximating-zero
 open import real-numbers.similarity-real-numbers
 open import real-numbers.squares-real-numbers
+open import real-numbers.strict-inequality-real-numbers
 ```
 
 </details>
@@ -181,6 +188,27 @@ abstract
   is-positive-power-ℝ⁺ 1 (_ , is-pos-x) = is-pos-x
   is-positive-power-ℝ⁺ (succ-ℕ n@(succ-ℕ _)) x⁺@(x , is-pos-x) =
     is-positive-mul-ℝ (is-positive-power-ℝ⁺ n x⁺) is-pos-x
+
+power-ℝ⁺ : {l : Level} → ℕ → ℝ⁺ l → ℝ⁺ l
+power-ℝ⁺ n x⁺@(x , _) = (power-ℝ n x , is-positive-power-ℝ⁺ n x⁺)
+```
+
+### Powers of nonnegative real numbers are nonnegative
+
+```agda
+abstract
+  is-nonnegative-power-ℝ⁰⁺ :
+    {l : Level} (n : ℕ) (x : ℝ⁰⁺ l) → is-nonnegative-ℝ (power-ℝ n (real-ℝ⁰⁺ x))
+  is-nonnegative-power-ℝ⁰⁺ {l} 0 _ =
+    is-nonnegative-real-ℝ⁰⁺ (raise-ℝ⁰⁺ l one-ℝ⁰⁺)
+  is-nonnegative-power-ℝ⁰⁺ 1 (x , is-nonneg-x) = is-nonneg-x
+  is-nonnegative-power-ℝ⁰⁺ (succ-ℕ n@(succ-ℕ _)) x⁰⁺@(x , is-nonneg-x) =
+    is-nonnegative-mul-ℝ
+      ( is-nonnegative-power-ℝ⁰⁺ n x⁰⁺)
+      ( is-nonneg-x)
+
+power-ℝ⁰⁺ : {l : Level} → ℕ → ℝ⁰⁺ l → ℝ⁰⁺ l
+power-ℝ⁰⁺ n x⁰⁺@(x , _) = (power-ℝ n x , is-nonnegative-power-ℝ⁰⁺ n x⁰⁺)
 ```
 
 ### Even powers of negative real numbers are positive
@@ -326,3 +354,80 @@ abstract
       ≤ abs-ℝ (power-ℝ (succ-ℕ n) y)
         by leq-eq-ℝ (ap abs-ℝ (inv (power-succ-ℝ n y)))
 ```
+
+### If `x` and `y` are nonnegative such that `x ≤ y`, then `xⁿ ≤ yⁿ`
+
+```agda
+abstract
+  preserves-leq-power-real-ℝ⁰⁺ :
+    {l1 l2 : Level} (n : ℕ) (x : ℝ⁰⁺ l1) (y : ℝ⁰⁺ l2) → leq-ℝ⁰⁺ x y →
+    leq-ℝ (power-ℝ n (real-ℝ⁰⁺ x)) (power-ℝ n (real-ℝ⁰⁺ y))
+  preserves-leq-power-real-ℝ⁰⁺ {l1} {l2} 0 _ _ _ =
+    leq-sim-ℝ
+      ( transitive-sim-ℝ _ one-ℝ _
+        ( sim-raise-ℝ l2 one-ℝ)
+        ( symmetric-sim-ℝ (sim-raise-ℝ l1 one-ℝ)))
+  preserves-leq-power-real-ℝ⁰⁺ (succ-ℕ n) x⁰⁺@(x , _) y⁰⁺@(y , _) x≤y =
+    let
+      open inequality-reasoning-Large-Poset ℝ-Large-Poset
+    in
+      chain-of-inequalities
+      power-ℝ (succ-ℕ n) x
+      ≤ power-ℝ n x *ℝ x
+        by leq-eq-ℝ (power-succ-ℝ n x)
+      ≤ power-ℝ n y *ℝ y
+        by
+          preserves-leq-mul-ℝ⁰⁺
+            ( power-ℝ⁰⁺ n x⁰⁺)
+            ( power-ℝ⁰⁺ n y⁰⁺)
+            ( x⁰⁺)
+            ( y⁰⁺)
+            ( preserves-leq-power-real-ℝ⁰⁺ n x⁰⁺ y⁰⁺ x≤y)
+            ( x≤y)
+      ≤ power-ℝ (succ-ℕ n) y
+        by leq-eq-ℝ (inv (power-succ-ℝ n y))
+```
+
+### If `|r| < 1`, then `rⁿ` approaches 0
+
+```agda
+abstract
+  is-zero-lim-power-le-one-abs-ℝ :
+    {l : Level} (r : ℝ l) → le-ℝ (abs-ℝ r) one-ℝ →
+    is-zero-limit-sequence-ℝ (λ n → power-ℝ n r)
+  is-zero-lim-power-le-one-abs-ℝ r |r|<1 =
+    let
+      open
+        do-syntax-trunc-Prop (is-zero-limit-prop-sequence-ℝ (λ n → power-ℝ n r))
+      open inequality-reasoning-Large-Poset ℝ-Large-Poset
+    in do
+      (ε , |r|<ε , ε<1ℝ) ← dense-rational-le-ℝ _ _ |r|<1
+      let
+        is-pos-ε =
+          reflects-is-positive-real-ℚ
+            ( is-positive-le-ℝ⁰⁺ (nonnegative-abs-ℝ r) (real-ℚ ε) |r|<ε)
+        ε⁺ = (ε , is-pos-ε)
+      is-zero-limit-sequence-leq-abs-rational-zero-limit-sequence-ℝ
+        ( λ n → power-ℝ n r)
+        ( (λ n → rational-ℚ⁺ (power-ℚ⁺ n ε⁺)) ,
+          is-zero-limit-power-le-one-ℚ⁺ ε⁺ (reflects-le-real-ℚ ε<1ℝ))
+        ( λ n →
+          chain-of-inequalities
+            abs-ℝ (power-ℝ n r)
+            ≤ abs-ℝ (power-ℝ n (real-ℚ ε))
+              by
+                preserves-leq-abs-power-ℝ
+                  ( n)
+                  ( r)
+                  ( real-ℚ ε)
+                  ( inv-tr
+                    ( leq-ℝ (abs-ℝ r))
+                    ( abs-real-ℝ⁺ (positive-real-ℚ⁺ ε⁺))
+                    ( leq-le-ℝ |r|<ε))
+            ≤ power-ℝ n (real-ℚ ε)
+              by leq-eq-ℝ (abs-real-ℝ⁺ (power-ℝ⁺ n (positive-real-ℚ⁺ ε⁺)))
+            ≤ real-ℚ (power-ℚ n ε)
+              by leq-eq-ℝ (power-real-ℚ n ε)
+            ≤ real-ℚ⁺ (power-ℚ⁺ n ε⁺)
+              by leq-eq-ℝ (ap real-ℚ (power-rational-ℚ⁺ n ε⁺)))
+```
diff --git a/src/real-numbers/real-sequences-approximating-zero.lagda.md b/src/real-numbers/real-sequences-approximating-zero.lagda.md
new file mode 100644
index 0000000000..4cf4a469c7
--- /dev/null
+++ b/src/real-numbers/real-sequences-approximating-zero.lagda.md
@@ -0,0 +1,114 @@
+# Real sequences approximating zero
+
+```agda
+{-# OPTIONS --lossy-unification #-}
+
+module real-numbers.real-sequences-approximating-zero where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.absolute-value-rational-numbers
+open import elementary-number-theory.distance-rational-numbers
+open import elementary-number-theory.natural-numbers
+open import elementary-number-theory.nonnegative-rational-numbers
+open import elementary-number-theory.rational-numbers
+
+open import foundation.action-on-identifications-functions
+open import foundation.dependent-pair-types
+open import foundation.existential-quantification
+open import foundation.function-types
+open import foundation.identity-types
+open import foundation.propositions
+open import foundation.universe-levels
+
+open import lists.sequences
+
+open import logic.functoriality-existential-quantification
+
+open import metric-spaces.limits-of-sequences-metric-spaces
+open import metric-spaces.metric-space-of-rational-numbers
+open import metric-spaces.rational-sequences-approximating-zero
+
+open import order-theory.large-posets
+
+open import real-numbers.absolute-value-real-numbers
+open import real-numbers.dedekind-real-numbers
+open import real-numbers.distance-real-numbers
+open import real-numbers.inequality-real-numbers
+open import real-numbers.limits-sequences-real-numbers
+open import real-numbers.metric-space-of-real-numbers
+open import real-numbers.raising-universe-levels-real-numbers
+open import real-numbers.rational-real-numbers
+open import real-numbers.similarity-real-numbers
+```
+
+</details>
+
+## Idea
+
+A [sequence](lists.sequences.md) of
+[real numbers](real-numbers.dedekind-real-numbers.md) is an
+{{#concept "approximation of zero" Disambiguation="sequence of real numbers" Agda=zero-limit-sequence-ℝ}}
+if it [converges](metric-spaces.limits-of-sequences-metric-spaces.md) to 0 in
+the
+[standard metric space of real numbers](real-numbers.metric-space-of-real-numbers.md).
+
+## Definition
+
+```agda
+is-zero-limit-prop-sequence-ℝ : {l : Level} → sequence (ℝ l) → Prop l
+is-zero-limit-prop-sequence-ℝ {l} σ =
+  is-limit-prop-sequence-ℝ σ (raise-ℝ l zero-ℝ)
+
+is-zero-limit-sequence-ℝ : {l : Level} → sequence (ℝ l) → UU l
+is-zero-limit-sequence-ℝ σ = type-Prop (is-zero-limit-prop-sequence-ℝ σ)
+```
+
+## Properties
+
+### If the absolute value of a sequence of reals is bounded by a rational approximation of zero, the sequence of reals is an approximation of zero
+
+```agda
+abstract
+  is-zero-limit-sequence-leq-abs-rational-zero-limit-sequence-ℝ :
+    {l : Level} (a : sequence (ℝ l)) (b : zero-limit-sequence-ℚ) →
+    ((n : ℕ) → leq-ℝ (abs-ℝ (a n)) (real-ℚ (seq-zero-limit-sequence-ℚ b n))) →
+    is-zero-limit-sequence-ℝ a
+  is-zero-limit-sequence-leq-abs-rational-zero-limit-sequence-ℝ
+    {l} a (b , lim-b=0) H =
+    let
+      open inequality-reasoning-Large-Poset ℝ-Large-Poset
+    in
+      map-tot-exists
+        ( λ μ is-mod-μ ε n με≤n →
+          neighborhood-dist-ℝ
+            ( ε)
+            ( a n)
+            ( raise-ℝ l zero-ℝ)
+            ( chain-of-inequalities
+              dist-ℝ (a n) (raise-ℝ l zero-ℝ)
+              ≤ dist-ℝ (a n) zero-ℝ
+                by
+                  leq-sim-ℝ
+                    ( preserves-dist-right-sim-ℝ
+                      ( symmetric-sim-ℝ (sim-raise-ℝ l zero-ℝ)))
+              ≤ abs-ℝ (a n)
+                by leq-eq-ℝ (right-zero-law-dist-ℝ (a n))
+              ≤ real-ℚ (b n)
+                by H n
+              ≤ real-ℚ (rational-abs-ℚ (b n))
+                by preserves-leq-real-ℚ (leq-abs-ℚ (b n))
+              ≤ real-ℚ (rational-dist-ℚ (b n) zero-ℚ)
+                by
+                  leq-eq-ℝ
+                    ( ap
+                      ( real-ℚ ∘ rational-ℚ⁰⁺)
+                      ( inv (right-zero-law-dist-ℚ (b n))))
+              ≤ real-ℚ⁺ ε
+                by
+                  preserves-leq-real-ℚ
+                    ( leq-dist-neighborhood-ℚ ε _ _ (is-mod-μ ε n με≤n))))
+        ( lim-b=0)
+```
diff --git a/src/real-numbers/series-real-numbers.lagda.md b/src/real-numbers/series-real-numbers.lagda.md
new file mode 100644
index 0000000000..f3d0ecf21e
--- /dev/null
+++ b/src/real-numbers/series-real-numbers.lagda.md
@@ -0,0 +1,42 @@
+# Series of real numbers
+
+```agda
+{-# OPTIONS --lossy-unification #-}
+
+module real-numbers.series-real-numbers where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import analysis.series-metric-abelian-groups
+
+open import foundation.universe-levels
+
+open import lists.sequences
+
+open import real-numbers.dedekind-real-numbers
+open import real-numbers.metric-abelian-group-of-real-numbers
+```
+
+</details>
+
+## Idea
+
+A {{#concept "series" Disambiguation="of real numbers" Agda=series-ℝ}} of
+[real numbers](real-numbers.dedekind-real-numbers.md) is an infinite sum
+$$∑_{n=0}^∞ a_n$$, which is evaluated for convergence in the
+[metric abelian group of real numbers](real-numbers.metric-abelian-group-of-real-numbers.md).
+
+## Definition
+
+```agda
+series-ℝ : (l : Level) → UU (lsuc l)
+series-ℝ l = series-Metric-Ab (metric-ab-ℝ l)
+
+series-terms-ℝ : {l : Level} → sequence (ℝ l) → series-ℝ l
+series-terms-ℝ = series-terms-Metric-Ab
+
+terms-series-ℝ : {l : Level} → series-ℝ l → sequence (ℝ l)
+terms-series-ℝ = term-series-Metric-Ab
+```
diff --git a/src/real-numbers/uniformly-continuous-functions-real-numbers.lagda.md b/src/real-numbers/uniformly-continuous-functions-real-numbers.lagda.md
new file mode 100644
index 0000000000..c929bb7da0
--- /dev/null
+++ b/src/real-numbers/uniformly-continuous-functions-real-numbers.lagda.md
@@ -0,0 +1,59 @@
+# Uniformly continuous functions of real numbers
+
+```agda
+{-# OPTIONS --lossy-unification #-}
+
+module real-numbers.uniformly-continuous-functions-real-numbers where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.universe-levels
+
+open import metric-spaces.uniformly-continuous-functions-metric-spaces
+
+open import real-numbers.dedekind-real-numbers
+open import real-numbers.metric-space-of-real-numbers
+```
+
+</details>
+
+## Idea
+
+A
+{{#concept "uniformly continuous function" Disambiguation="from ℝ to ℝ" Agda=uniformly-continuous-function-ℝ}}
+from the [real numbers](real-numbers.dedekind-real-numbers.md) to the real
+numbers is a function `f : ℝ → ℝ` such that there
+[exists](foundation.existential-quantification.md) a modulus `μ : ℚ⁺ → ℚ⁺` such
+that for all `x y : ℝ` within a
+`μ ε`-[neighborhood](real-numbers.metric-space-of-real-numbers.md) of each
+other, `f x` and `f y` are within an `ε`-neighborhood.
+
+## Definition
+
+```agda
+uniformly-continuous-function-ℝ : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2)
+uniformly-continuous-function-ℝ l1 l2 =
+  uniformly-continuous-function-Metric-Space
+    ( metric-space-ℝ l1)
+    ( metric-space-ℝ l2)
+
+comp-uniformly-continuous-function-ℝ :
+  {l1 l2 l3 : Level} →
+  uniformly-continuous-function-ℝ l2 l3 →
+  uniformly-continuous-function-ℝ l1 l2 →
+  uniformly-continuous-function-ℝ l1 l3
+comp-uniformly-continuous-function-ℝ {l1} {l2} {l3} =
+  comp-uniformly-continuous-function-Metric-Space
+    ( metric-space-ℝ l1)
+    ( metric-space-ℝ l2)
+    ( metric-space-ℝ l3)
+
+map-uniformly-continuous-function-ℝ :
+  {l1 l2 : Level} → uniformly-continuous-function-ℝ l1 l2 → ℝ l1 → ℝ l2
+map-uniformly-continuous-function-ℝ {l1} {l2} =
+  map-uniformly-continuous-function-Metric-Space
+    ( metric-space-ℝ l1)
+    ( metric-space-ℝ l2)
+```