diff --git a/src/elementary-number-theory/bezouts-lemma-natural-numbers.lagda.md b/src/elementary-number-theory/bezouts-lemma-natural-numbers.lagda.md index 407b072465..aa063d02c4 100755 --- a/src/elementary-number-theory/bezouts-lemma-natural-numbers.lagda.md +++ b/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)) diff --git a/src/elementary-number-theory/divisibility-natural-numbers.lagda.md b/src/elementary-number-theory/divisibility-natural-numbers.lagda.md index 9bf81abc22..f0f1d29264 100644 --- a/src/elementary-number-theory/divisibility-natural-numbers.lagda.md +++ b/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)) diff --git a/src/elementary-number-theory/fundamental-theorem-of-arithmetic.lagda.md b/src/elementary-number-theory/fundamental-theorem-of-arithmetic.lagda.md index 33989ff00a..e02ec45104 100644 --- a/src/elementary-number-theory/fundamental-theorem-of-arithmetic.lagda.md +++ b/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) diff --git a/src/elementary-number-theory/greatest-common-divisor-natural-numbers.lagda.md b/src/elementary-number-theory/greatest-common-divisor-natural-numbers.lagda.md index 8bb0394585..f759f47afb 100644 --- a/src/elementary-number-theory/greatest-common-divisor-natural-numbers.lagda.md +++ b/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))) ``` diff --git a/src/elementary-number-theory/inequality-standard-finite-types.lagda.md b/src/elementary-number-theory/inequality-standard-finite-types.lagda.md index d21985ad6f..aee581051e 100644 --- a/src/elementary-number-theory/inequality-standard-finite-types.lagda.md +++ b/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 ``` diff --git a/src/elementary-number-theory/infinitude-of-primes.lagda.md b/src/elementary-number-theory/infinitude-of-primes.lagda.md index 975d16b0b2..46f2081371 100644 --- a/src/elementary-number-theory/infinitude-of-primes.lagda.md +++ b/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) diff --git a/src/elementary-number-theory/strict-inequality-integer-fractions.lagda.md b/src/elementary-number-theory/strict-inequality-integer-fractions.lagda.md index d58fbf1f4c..35c105a595 100644 --- a/src/elementary-number-theory/strict-inequality-integer-fractions.lagda.md +++ b/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 diff --git a/src/elementary-number-theory/strict-inequality-integers.lagda.md b/src/elementary-number-theory/strict-inequality-integers.lagda.md index 107592ee5c..105830da9d 100644 --- a/src/elementary-number-theory/strict-inequality-integers.lagda.md +++ b/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 diff --git a/src/elementary-number-theory/strict-inequality-natural-numbers.lagda.md b/src/elementary-number-theory/strict-inequality-natural-numbers.lagda.md index dc859952a8..5c2668d936 100644 --- a/src/elementary-number-theory/strict-inequality-natural-numbers.lagda.md +++ b/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` diff --git a/src/elementary-number-theory/strict-inequality-rational-numbers.lagda.md b/src/elementary-number-theory/strict-inequality-rational-numbers.lagda.md index 99d4619055..eddcd5f15f 100644 --- a/src/elementary-number-theory/strict-inequality-rational-numbers.lagda.md +++ b/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 diff --git a/src/finite-group-theory/orbits-permutations.lagda.md b/src/finite-group-theory/orbits-permutations.lagda.md index 4b629bb9c1..a76f4c5ab9 100644 --- a/src/finite-group-theory/orbits-permutations.lagda.md +++ b/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)) diff --git a/src/univalent-combinatorics/pigeonhole-principle.lagda.md b/src/univalent-combinatorics/pigeonhole-principle.lagda.md index 8c52386070..35499de258 100644 --- a/src/univalent-combinatorics/pigeonhole-principle.lagda.md +++ b/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