Update src/elementary-number-theory/inequality-integers.lagda.md

Co-authored-by: Fredrik Bakke <[email protected]>
UniMath · Feb 27, 2024 · b1fd714 · b1fd714
1 parent ff43290
commit b1fd714
Showing 1 changed file with 6 additions and 6 deletions.
diff --git a/src/elementary-number-theory/inequality-integers.lagda.md b/src/elementary-number-theory/inequality-integers.lagda.md
@@ -123,12 +123,12 @@ transitive-le-ℤ k l m p q =
 asymmetric-le-ℤ : (x y : ℤ) → le-ℤ x y → ¬ (le-ℤ y x)
 asymmetric-le-ℤ x y p q =
   not-is-nonpositive-is-positive-ℤ
-  ( y -ℤ x)
-  ( p)
-  ( is-nonnegative-is-positive-ℤ
-    ( is-positive-eq-ℤ
-      ( inv ( distributive-neg-diff-ℤ y x))
-      ( q)))
+    ( y -ℤ x)
+    ( p)
+    ( is-nonnegative-is-positive-ℤ
+      ( is-positive-eq-ℤ
+        ( inv ( distributive-neg-diff-ℤ y x))
+        ( q)))
 
 connected-le-ℤ : (x y : ℤ) → x ≠ y → le-ℤ x y + le-ℤ y x
 connected-le-ℤ x y H =