Addition on real numbers

src/elementary-number-theory/positive-rational-numbers.lagda.md

@@ -205,13 +205,14 @@ module _
   (x y : ℚ) (H : le-ℚ x y)
   where
 
-  is-positive-diff-le-ℚ : is-positive-ℚ (y -ℚ x)
-  is-positive-diff-le-ℚ =
-    is-positive-le-zero-ℚ
-      ( y -ℚ x)
-      ( backward-implication
-        ( iff-translate-diff-le-zero-ℚ x y)
-        ( H))
+  abstract
+    is-positive-diff-le-ℚ : is-positive-ℚ (y -ℚ x)
+    is-positive-diff-le-ℚ =
+      is-positive-le-zero-ℚ
+        ( y -ℚ x)
+        ( backward-implication
+          ( iff-translate-diff-le-zero-ℚ x y)
+          ( H))
 
   positive-diff-le-ℚ : ℚ⁺
   positive-diff-le-ℚ = y -ℚ x , is-positive-diff-le-ℚ
@@ -620,12 +621,13 @@ mediant-zero-ℚ⁺ x =
         ( rational-ℚ⁺ x)
         ( le-zero-is-positive-ℚ (rational-ℚ⁺ x) (is-positive-rational-ℚ⁺ x))))
 
-le-mediant-zero-ℚ⁺ : (x : ℚ⁺) → le-ℚ⁺ (mediant-zero-ℚ⁺ x) x
-le-mediant-zero-ℚ⁺ x =
-  le-right-mediant-ℚ
-    ( zero-ℚ)
-    ( rational-ℚ⁺ x)
-    ( le-zero-is-positive-ℚ (rational-ℚ⁺ x) (is-positive-rational-ℚ⁺ x))
+abstract
+  le-mediant-zero-ℚ⁺ : (x : ℚ⁺) → le-ℚ⁺ (mediant-zero-ℚ⁺ x) x
+  le-mediant-zero-ℚ⁺ x =
+    le-right-mediant-ℚ
+      ( zero-ℚ)
+      ( rational-ℚ⁺ x)
+      ( le-zero-is-positive-ℚ (rational-ℚ⁺ x) (is-positive-rational-ℚ⁺ x))
 ```
 
 ### Any positive rational number is the sum of two positive rational numbers

src/elementary-number-theory/strict-inequality-rational-numbers.lagda.md

@@ -127,12 +127,13 @@ module _
   (x y z : ℚ)
   where
 
-  transitive-le-ℚ : le-ℚ y z → le-ℚ x y → le-ℚ x z
-  transitive-le-ℚ =
-    transitive-le-fraction-ℤ
-      ( fraction-ℚ x)
-      ( fraction-ℚ y)
-      ( fraction-ℚ z)
+  abstract
+    transitive-le-ℚ : le-ℚ y z → le-ℚ x y → le-ℚ x z
+    transitive-le-ℚ =
+      transitive-le-fraction-ℤ
+        ( fraction-ℚ x)
+        ( fraction-ℚ y)
+        ( fraction-ℚ z)
 ```
 
 ### Concatenation rules for inequality and strict inequality on the rational numbers
@@ -320,15 +321,16 @@ module _
 ### Addition on the rational numbers preserves strict inequality
 
 ```agda
-preserves-le-add-ℚ :
-  {a b c d : ℚ} → le-ℚ a b → le-ℚ c d → le-ℚ (a +ℚ c) (b +ℚ d)
-preserves-le-add-ℚ {a} {b} {c} {d} H K =
-  transitive-le-ℚ
-    ( a +ℚ c)
-    ( b +ℚ c)
-    ( b +ℚ d)
-    ( preserves-le-right-add-ℚ b c d K)
-    ( preserves-le-left-add-ℚ c a b H)
+abstract
+  preserves-le-add-ℚ :
+    {a b c d : ℚ} → le-ℚ a b → le-ℚ c d → le-ℚ (a +ℚ c) (b +ℚ d)
+  preserves-le-add-ℚ {a} {b} {c} {d} H K =
+    transitive-le-ℚ
+      ( a +ℚ c)
+      ( b +ℚ c)
+      ( b +ℚ d)
+      ( preserves-le-right-add-ℚ b c d K)
+      ( preserves-le-left-add-ℚ c a b H)
 ```
 
 ### The rational numbers have no lower or upper bound

src/group-theory/abelian-groups.lagda.md

@@ -612,17 +612,18 @@ module _
   {l : Level} (A : Ab l)
   where
 
-  is-identity-left-conjugation-Ab :
-    (x : type-Ab A) → left-conjugation-Ab A x ~ id
-  is-identity-left-conjugation-Ab x y =
-    ( ap (add-Ab' A (neg-Ab A x)) (commutative-add-Ab A x y)) ∙
-    ( is-retraction-right-subtraction-Ab A x y)
-
-  is-identity-right-conjugation-Ab :
-    (x : type-Ab A) → right-conjugation-Ab A x ~ id
-  is-identity-right-conjugation-Ab x =
-    inv-htpy (left-right-conjugation-Ab A x) ∙h
-    is-identity-left-conjugation-Ab x
+  abstract
+    is-identity-left-conjugation-Ab :
+      (x : type-Ab A) → left-conjugation-Ab A x ~ id
+    is-identity-left-conjugation-Ab x y =
+      ( ap (add-Ab' A (neg-Ab A x)) (commutative-add-Ab A x y)) ∙
+      ( is-retraction-right-subtraction-Ab A x y)
+
+    is-identity-right-conjugation-Ab :
+      (x : type-Ab A) → right-conjugation-Ab A x ~ id
+    is-identity-right-conjugation-Ab x =
+      inv-htpy (left-right-conjugation-Ab A x) ∙h
+      is-identity-left-conjugation-Ab x
 
   is-identity-conjugation-Ab :
     (x : type-Ab A) → conjugation-Ab A x ~ id

src/real-numbers.lagda.md

@@ -6,10 +6,12 @@
 module real-numbers where
 
 open import real-numbers.addition-lower-dedekind-real-numbers public
+open import real-numbers.addition-real-numbers public
 open import real-numbers.addition-upper-dedekind-real-numbers public
 open import real-numbers.apartness-real-numbers public
 open import real-numbers.arithmetically-located-dedekind-cuts public
 open import real-numbers.dedekind-real-numbers public
+open import real-numbers.difference-real-numbers public
 open import real-numbers.inequality-lower-dedekind-real-numbers public
 open import real-numbers.inequality-real-numbers public
 open import real-numbers.inequality-upper-dedekind-real-numbers public