Make naturals, integers, integer fractions, and rationals consistent about some inequality theorems

src/elementary-number-theory/bezouts-lemma-natural-numbers.lagda.md

@@ -1308,7 +1308,7 @@ remainder-min-dist-succ-x-is-distance x y =
 
     quotient-min-dist-succ-x-nonzero : is-nonzero-ℕ q
     quotient-min-dist-succ-x-nonzero iszero =
-      contradiction-le-ℕ (succ-ℕ x) d le-x-d leq-d-x
+      not-leq-le-ℕ (succ-ℕ x) d le-x-d leq-d-x
       where
       x-r-equality : succ-ℕ x ＝ r
       x-r-equality =
@@ -1721,7 +1721,7 @@ remainder-min-dist-succ-x-is-not-nonzero :
         ( minimal-positive-distance (succ-ℕ x) y)
         ( succ-ℕ x)))
 remainder-min-dist-succ-x-is-not-nonzero x y nonzero =
-  contradiction-le-ℕ
+  not-leq-le-ℕ
     ( remainder-euclidean-division-ℕ
       ( minimal-positive-distance (succ-ℕ x) y)
       ( succ-ℕ x))

src/elementary-number-theory/divisibility-natural-numbers.lagda.md

@@ -254,7 +254,7 @@ is-zero-div-ℕ :
 is-zero-div-ℕ d zero-ℕ H D = refl
 is-zero-div-ℕ d (succ-ℕ x) H (pair (succ-ℕ k) p) =
   ex-falso
-    ( contradiction-le-ℕ
+    ( not-leq-le-ℕ
       ( succ-ℕ x) d H
       ( concatenate-leq-eq-ℕ d
         ( leq-add-ℕ' d (k *ℕ d)) p))

src/elementary-number-theory/fundamental-theorem-of-arithmetic.lagda.md

@@ -344,7 +344,7 @@ pr1 (is-prime-least-nontrivial-divisor-ℕ n H x) (K , L) =
     ( is-one-ℕ x)
     ( le-ℕ 1 x)
     ( λ p →
-      contradiction-le-ℕ x l
+      not-leq-le-ℕ x l
         ( le-div-ℕ x l
           ( is-nonzero-least-nontrivial-divisor-ℕ n H)
           ( L)
@@ -746,7 +746,7 @@ is-in-prime-decomposition-is-nontrivial-prime-divisor-ℕ :
   y ∈-list l
 is-in-prime-decomposition-is-nontrivial-prime-divisor-ℕ x H nil D y d p =
   ex-falso
-    ( contradiction-le-ℕ
+    ( not-leq-le-ℕ
       ( 1)
       ( x)
       ( concatenate-le-leq-ℕ
@@ -874,7 +874,7 @@ eq-prime-decomposition-list-ℕ x H nil nil _ _ =
   refl
 eq-prime-decomposition-list-ℕ x H (cons y l) nil I J =
   ex-falso
-    ( contradiction-le-ℕ
+    ( not-leq-le-ℕ
       ( 1)
       ( x)
       ( le-one-is-nonempty-prime-decomposition-list-ℕ x H y l I)
@@ -884,7 +884,7 @@ eq-prime-decomposition-list-ℕ x H (cons y l) nil I J =
         ( inv ( is-decomposition-list-is-prime-decomposition-list-ℕ x nil J))))
 eq-prime-decomposition-list-ℕ x H nil (cons y l) I J =
   ex-falso
-    ( contradiction-le-ℕ
+    ( not-leq-le-ℕ
       ( 1)
       ( x)
       ( le-one-is-nonempty-prime-decomposition-list-ℕ x H y l J)

src/elementary-number-theory/greatest-common-divisor-natural-numbers.lagda.md

@@ -242,7 +242,7 @@ is-zero-is-common-divisor-le-gcd-ℕ a b r l d with is-decidable-is-zero-ℕ r
 ... | inl H = H
 ... | inr x =
   ex-falso
-    ( contradiction-le-ℕ r (gcd-ℕ a b) l
+    ( not-leq-le-ℕ r (gcd-ℕ a b) l
       ( is-lower-bound-gcd-ℕ a b r (λ np → pair x d)))
 ```
 

src/elementary-number-theory/inequality-standard-finite-types.lagda.md

@@ -99,7 +99,7 @@ reflects-leq-nat-Fin (succ-ℕ k) {inl x} {inl y} H =
   reflects-leq-nat-Fin k H
 reflects-leq-nat-Fin (succ-ℕ k) {inr star} {inl y} H =
   ex-falso
-    ( contradiction-le-ℕ (nat-Fin k y) k (strict-upper-bound-nat-Fin k y) H)
+    ( not-leq-le-ℕ (nat-Fin k y) k (strict-upper-bound-nat-Fin k y) H)
 reflects-leq-nat-Fin (succ-ℕ k) {inl x} {inr star} H = star
 reflects-leq-nat-Fin (succ-ℕ k) {inr star} {inr star} H = star
 ```

src/elementary-number-theory/infinitude-of-primes.lagda.md

@@ -111,12 +111,13 @@ not-in-sieve-of-eratosthenes-is-proper-divisor-larger-prime-ℕ :
   (n x : ℕ) → is-proper-divisor-ℕ (larger-prime-ℕ n) x →
   ¬ (in-sieve-of-eratosthenes-ℕ n x)
 not-in-sieve-of-eratosthenes-is-proper-divisor-larger-prime-ℕ n x H K =
-  ex-falso
-    ( contradiction-le-ℕ x (larger-prime-ℕ n)
-      ( le-is-proper-divisor-ℕ x (larger-prime-ℕ n)
-        ( is-nonzero-larger-prime-ℕ n)
-        ( H))
-      ( is-lower-bound-larger-prime-ℕ n x K))
+  not-leq-le-ℕ
+    ( x)
+    ( larger-prime-ℕ n)
+    ( le-is-proper-divisor-ℕ x (larger-prime-ℕ n)
+      ( is-nonzero-larger-prime-ℕ n)
+      ( H))
+    ( is-lower-bound-larger-prime-ℕ n x K)
 
 is-one-is-proper-divisor-larger-prime-ℕ :
   (n : ℕ) → is-nonzero-ℕ n → is-one-is-proper-divisor-ℕ (larger-prime-ℕ n)

src/elementary-number-theory/strict-inequality-integer-fractions.lagda.md

@@ -91,13 +91,9 @@ le-fraction-ℤ-Decidable-Prop x y =
 decide-le-leq-fraction-ℤ :
   (x y : fraction-ℤ) → le-fraction-ℤ x y + leq-fraction-ℤ y x
 decide-le-leq-fraction-ℤ x y =
-  map-coproduct
-    ( id)
-    ( λ H →
-      is-nonnegative-eq-ℤ
-        ( skew-commutative-cross-mul-diff-fraction-ℤ x y)
-        ( is-nonnegative-neg-is-nonpositive-ℤ H))
-    ( decide-is-positive-is-nonpositive-ℤ)
+  decide-le-leq-ℤ
+    ( numerator-fraction-ℤ x *ℤ denominator-fraction-ℤ y)
+    ( numerator-fraction-ℤ y *ℤ denominator-fraction-ℤ x)
 ```
 
 ### Strict inequality on the integer fractions implies inequality
@@ -342,6 +338,29 @@ module _
             ( denominator-fraction-ℤ y))))
 ```
 
+### If `x < y` then `y ≰ x`
+
+```agda
+not-leq-le-fraction-ℤ :
+  (x y : fraction-ℤ) →
+  le-fraction-ℤ x y →
+  ¬ (leq-fraction-ℤ y x)
+not-leq-le-fraction-ℤ x y =
+  not-leq-le-ℤ
+    ( numerator-fraction-ℤ x *ℤ denominator-fraction-ℤ y)
+    ( numerator-fraction-ℤ y *ℤ denominator-fraction-ℤ x)
+```
+
+### If `x ≤ y` then `y ≮ x`
+
+```agda
+not-le-leq-fraction-ℤ :
+  (x y : fraction-ℤ) →
+  leq-fraction-ℤ x y →
+  ¬ (le-fraction-ℤ y x)
+not-le-leq-fraction-ℤ x y K H = not-leq-le-fraction-ℤ y x H K
+```
+
 ### Negation reverses the order of strict inequality on integer fractions
 
 ```agda

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

@@ -270,6 +270,40 @@ module _
           ( I))
 ```
 
+### For any two integers `x` and `y`, either `x < y` or `y ≤ x`
+
+```agda
+decide-le-leq-ℤ : (x y : ℤ) → le-ℤ x y + leq-ℤ y x
+decide-le-leq-ℤ x y with decide-is-negative-is-nonnegative-ℤ {x -ℤ y}
+... | inr x-y-nonneg = inr x-y-nonneg
+... | inl x-y-neg =
+  inl
+    ( tr
+      ( is-positive-ℤ)
+      ( distributive-neg-diff-ℤ x y)
+      ( is-positive-neg-is-negative-ℤ x-y-neg))
+```
+
+### If `m < n` then `n ≰ m`
+
+```agda
+not-leq-le-ℤ : (m n : ℤ) → le-ℤ m n → ¬ (n ≤-ℤ m)
+not-leq-le-ℤ m n n-m-is-positive m-n-is-nonnegative =
+  is-not-positive-is-nonpositive-ℤ
+    ( tr
+      ( is-nonpositive-ℤ)
+      ( distributive-neg-diff-ℤ m n)
+      ( is-nonpositive-neg-is-nonnegative-ℤ m-n-is-nonnegative))
+    ( n-m-is-positive)
+```
+
+### If `n ≤ m` then `m ≮ n`
+
+```agda
+not-le-leq-ℤ : (m n : ℤ) → n ≤-ℤ m → ¬ (le-ℤ m n)
+not-le-leq-ℤ m n K H = not-leq-le-ℤ m n H K
+```
+
 ### The inclusion of natural numbers preserves strict inequality
 
 ```agda

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

@@ -231,16 +231,16 @@ concatenate-le-leq-ℕ {succ-ℕ x} {succ-ℕ y} {succ-ℕ z} H K =
 ### If `m < n` then `n ≰ m`
 
 ```agda
-contradiction-le-ℕ : (m n : ℕ) → le-ℕ m n → ¬ (n ≤-ℕ m)
-contradiction-le-ℕ zero-ℕ (succ-ℕ n) H K = K
-contradiction-le-ℕ (succ-ℕ m) (succ-ℕ n) H = contradiction-le-ℕ m n H
+not-leq-le-ℕ : (m n : ℕ) → le-ℕ m n → ¬ (n ≤-ℕ m)
+not-leq-le-ℕ zero-ℕ (succ-ℕ n) H K = K
+not-leq-le-ℕ (succ-ℕ m) (succ-ℕ n) H = not-leq-le-ℕ m n H
 ```
 
 ### If `n ≤ m` then `m ≮ n`
 
 ```agda
-contradiction-le-ℕ' : (m n : ℕ) → n ≤-ℕ m → ¬ (le-ℕ m n)
-contradiction-le-ℕ' m n K H = contradiction-le-ℕ m n H K
+not-le-leq-ℕ : (m n : ℕ) → n ≤-ℕ m → ¬ (le-ℕ m n)
+not-le-leq-ℕ m n K H = not-leq-le-ℕ m n H K
 ```
 
 ### If `m ≮ n` then `n ≤ m`

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

@@ -378,15 +378,10 @@ decide-le-leq-ℚ x y =
     ( decide-is-positive-is-nonpositive-ℤ)
 
 not-leq-le-ℚ : (x y : ℚ) → le-ℚ x y → ¬ leq-ℚ y x
-not-leq-le-ℚ x y H K =
-  is-not-positive-is-nonpositive-ℤ
-    ( tr
-      ( is-nonpositive-ℤ)
-      ( skew-commutative-cross-mul-diff-fraction-ℤ
-        ( fraction-ℚ y)
-        ( fraction-ℚ x))
-      ( is-nonpositive-neg-is-nonnegative-ℤ K))
-    ( H)
+not-leq-le-ℚ x y = not-leq-le-fraction-ℤ (fraction-ℚ x) (fraction-ℚ y)
+
+not-le-leq-ℚ : (x y : ℚ) → leq-ℚ x y → ¬ le-ℚ y x
+not-le-leq-ℚ x y = not-le-leq-fraction-ℤ (fraction-ℚ x) (fraction-ℚ y)
 ```
 
 ### Trichotomy on the rationals

src/finite-group-theory/orbits-permutations.lagda.md

@@ -262,7 +262,7 @@ module _
     not-not-eq-second-point-zero-min-reporting :
       ¬¬ (Id second-point-min-repeating zero-ℕ)
     not-not-eq-second-point-zero-min-reporting np =
-      contradiction-le-ℕ
+      not-leq-le-ℕ
         ( pred-first)
         ( first-point-min-repeating)
         ( tr
@@ -881,7 +881,7 @@ module _
         ( is-nonzero-ℕ k × le-ℕ k (pr1 (minimal-element-iterate g a b pa))) →
         ( iterate k (map-equiv g) a ≠ a) × (iterate k (map-equiv g) a ≠ b)
       pr1 (neq-iterate-nonzero-le-minimal-element pa k (pair nz ineq)) q =
-        contradiction-le-ℕ
+        not-leq-le-ℕ
           ( pr1 pair-k2)
           ( pr1 (minimal-element-iterate g a b pa))
           ( le-subtraction-ℕ
@@ -909,7 +909,7 @@ module _
           (subtraction-le-ℕ k (pr1 (minimal-element-iterate g a b pa)) ineq)
       pr2 (neq-iterate-nonzero-le-minimal-element pa k (pair nz ineq)) r =
         ex-falso
-          ( contradiction-le-ℕ k (pr1 (minimal-element-iterate g a b pa))
+          ( not-leq-le-ℕ k (pr1 (minimal-element-iterate g a b pa))
             ineq (pr2 (pr2 (minimal-element-iterate g a b pa)) k r))
       equal-iterate-transposition-a :
         (pa : Σ ℕ (λ k → Id (iterate k (map-equiv g) a) b)) (k : ℕ) →
@@ -1018,7 +1018,7 @@ module _
         ( pa : Σ ℕ (λ k → Id (iterate k (map-equiv g) a) b)) (k : ℕ) →
         iterate k (map-equiv (composition-transposition-a-b g)) a ≠ b
       lemma3 pa k q =
-        contradiction-le-ℕ
+        not-leq-le-ℕ
           ( r)
           ( pr1 (minimal-element-iterate g a b pa))
           ( ineq)
@@ -1180,12 +1180,12 @@ module _
           ( λ k' p →
             pair
               ( λ q →
-                contradiction-le-ℕ k'
+                not-leq-le-ℕ k'
                   ( pr1 (minimal-element-iterate-2-a-b g pa))
                   ( p)
                   ( pr2 (pr2 (minimal-element-iterate-2-a-b g pa)) k' (inl q)))
               ( λ r →
-                contradiction-le-ℕ k'
+                not-leq-le-ℕ k'
                   ( pr1 (minimal-element-iterate-2-a-b g pa))
                   ( p)
                   ( pr2 (pr2 (minimal-element-iterate-2-a-b g pa)) k' (inr r))))
@@ -2192,7 +2192,7 @@ module _
         is-nonzero-ℕ k × le-ℕ k (pr1 minimal-element-iterate-repeating) →
         (iterate k (map-equiv g) a ≠ a) × (iterate k (map-equiv g) a ≠ b)
       pr1 (neq-iterate-nonzero-le-minimal-element k (pair nz ineq)) Q =
-        contradiction-le-ℕ k (pr1 minimal-element-iterate-repeating) ineq
+        not-leq-le-ℕ k (pr1 minimal-element-iterate-repeating) ineq
           (pr2 (pr2 minimal-element-iterate-repeating) k (pair nz Q))
       pr2 (neq-iterate-nonzero-le-minimal-element k (pair nz ineq)) R =
         NP (unit-trunc-Prop (pair k R))

src/univalent-combinatorics/pigeonhole-principle.lagda.md

@@ -78,7 +78,7 @@ leq-is-injective-Fin k l H =
 is-not-emb-le-Fin :
   (k l : ℕ) (f : Fin k → Fin l) → le-ℕ l k → ¬ (is-emb f)
 is-not-emb-le-Fin k l f p =
-  map-neg (leq-is-emb-Fin k l) (contradiction-le-ℕ l k p)
+  map-neg (leq-is-emb-Fin k l) (not-leq-le-ℕ l k p)
 ```
 
 #### If `l < k`, then any map `f : Fin k → Fin l` is not injective