Strict inequality on the integer fractions

Content created by Fredrik Bakke, malarbol and Egbert Rijke.

Created on 2024-03-28.
Last modified on 2024-04-25.

module elementary-number-theory.strict-inequality-integer-fractions where
Imports 
open import elementary-number-theory.addition-integer-fractions
open import elementary-number-theory.addition-integers
open import elementary-number-theory.addition-positive-and-negative-integers
open import elementary-number-theory.cross-multiplication-difference-integer-fractions
open import elementary-number-theory.difference-integers
open import elementary-number-theory.inequality-integer-fractions
open import elementary-number-theory.inequality-integers
open import elementary-number-theory.integer-fractions
open import elementary-number-theory.integers
open import elementary-number-theory.mediant-integer-fractions
open import elementary-number-theory.multiplication-integers
open import elementary-number-theory.multiplication-positive-and-negative-integers
open import elementary-number-theory.nonnegative-integers
open import elementary-number-theory.nonpositive-integers
open import elementary-number-theory.positive-and-negative-integers
open import elementary-number-theory.positive-integers
open import elementary-number-theory.strict-inequality-integers

open import foundation.action-on-identifications-functions
open import foundation.cartesian-product-types
open import foundation.conjunction
open import foundation.coproduct-types
open import foundation.decidable-propositions
open import foundation.dependent-pair-types
open import foundation.disjunction
open import foundation.existential-quantification
open import foundation.function-types
open import foundation.functoriality-coproduct-types
open import foundation.identity-types
open import foundation.negation
open import foundation.propositional-truncations
open import foundation.propositions
open import foundation.transport-along-identifications
open import foundation.universe-levels

Idea

An integer fraction m/n is strictly less than the fraction m'/n' if the integer product m * n' is strictly less than m' * n.

Definition

Strict inequality on the integer fractions

le-fraction-ℤ-Prop : fraction-ℤ → fraction-ℤ → Prop lzero
le-fraction-ℤ-Prop (m , n , p) (m' , n' , p') =
  le-ℤ-Prop (m *ℤ n') (m' *ℤ n)

le-fraction-ℤ : fraction-ℤ → fraction-ℤ → UU lzero
le-fraction-ℤ x y = type-Prop (le-fraction-ℤ-Prop x y)

is-prop-le-fraction-ℤ : (x y : fraction-ℤ) → is-prop (le-fraction-ℤ x y)
is-prop-le-fraction-ℤ x y = is-prop-type-Prop (le-fraction-ℤ-Prop x y)

Properties

Strict inequality on the integer fractions is decidable

is-decidable-le-fraction-ℤ :
  (x y : fraction-ℤ) → (le-fraction-ℤ x y) + ¬ (le-fraction-ℤ x y)
is-decidable-le-fraction-ℤ x y =
  is-decidable-le-ℤ
    ( numerator-fraction-ℤ x *ℤ denominator-fraction-ℤ y)
    ( numerator-fraction-ℤ y *ℤ denominator-fraction-ℤ x)

le-fraction-ℤ-Decidable-Prop : (x y : fraction-ℤ) → Decidable-Prop lzero
le-fraction-ℤ-Decidable-Prop x y =
  ( le-fraction-ℤ x y ,
    is-prop-le-fraction-ℤ x y ,
    is-decidable-le-fraction-ℤ 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-ℤ)

Strict inequality on the integer fractions implies inequality

leq-le-fraction-ℤ : {x y : fraction-ℤ} → le-fraction-ℤ x y → leq-fraction-ℤ x y
leq-le-fraction-ℤ {x} {y} =
  leq-le-ℤ
    { mul-ℤ (numerator-fraction-ℤ x) (denominator-fraction-ℤ y)}
    { mul-ℤ (numerator-fraction-ℤ y) (denominator-fraction-ℤ x)}

Strict inequality on the integer fractions is asymmetric

module _
  (x y : fraction-ℤ)
  where

  asymmetric-le-fraction-ℤ :
    le-fraction-ℤ x y → ¬ (le-fraction-ℤ y x)
  asymmetric-le-fraction-ℤ =
    asymmetric-le-ℤ
      ( mul-ℤ
        ( numerator-fraction-ℤ x)
        ( denominator-fraction-ℤ y))
      ( mul-ℤ
        ( numerator-fraction-ℤ y)
        ( denominator-fraction-ℤ x))

Strict inequality on the integer fractions is transitive

transitive-le-fraction-ℤ :
  (p q r : fraction-ℤ) →
  le-fraction-ℤ q r →
  le-fraction-ℤ p q →
  le-fraction-ℤ p r
transitive-le-fraction-ℤ p q r H H' =
  is-positive-right-factor-mul-ℤ
    ( is-positive-eq-ℤ
      ( lemma-add-cross-mul-diff-fraction-ℤ p q r)
      ( is-positive-add-ℤ
        ( is-positive-mul-ℤ
          ( is-positive-denominator-fraction-ℤ p)
          ( H))
        ( is-positive-mul-ℤ
          ( is-positive-denominator-fraction-ℤ r)
          ( H'))))
      ( is-positive-denominator-fraction-ℤ q)

Chaining rules for inequality and strict inequality on the integer fractions

module _
  (p q r : fraction-ℤ)
  where

  concatenate-le-leq-fraction-ℤ :
    le-fraction-ℤ p q →
    leq-fraction-ℤ q r →
    le-fraction-ℤ p r
  concatenate-le-leq-fraction-ℤ H H' =
    is-positive-right-factor-mul-ℤ
      ( is-positive-eq-ℤ
        ( lemma-add-cross-mul-diff-fraction-ℤ p q r)
        ( is-positive-add-nonnegative-positive-ℤ
          ( is-nonnegative-mul-ℤ
            ( is-nonnegative-is-positive-ℤ
              ( is-positive-denominator-fraction-ℤ p))
            ( H'))
          ( is-positive-mul-ℤ
            ( is-positive-denominator-fraction-ℤ r)
            ( H))))
      ( is-positive-denominator-fraction-ℤ q)

  concatenate-leq-le-fraction-ℤ :
    leq-fraction-ℤ p q →
    le-fraction-ℤ q r →
    le-fraction-ℤ p r
  concatenate-leq-le-fraction-ℤ H H' =
    is-positive-right-factor-mul-ℤ
      ( is-positive-eq-ℤ
        ( lemma-add-cross-mul-diff-fraction-ℤ p q r)
        ( is-positive-add-positive-nonnegative-ℤ
          ( is-positive-mul-ℤ
            ( is-positive-denominator-fraction-ℤ p)
            ( H'))
          ( is-nonnegative-mul-ℤ
            ( is-nonnegative-is-positive-ℤ
              ( is-positive-denominator-fraction-ℤ r))
            ( H))))
      ( is-positive-denominator-fraction-ℤ q)

Chaining rules for similarity and strict inequality on the integer fractions

module _
  (p q r : fraction-ℤ)
  where

  concatenate-sim-le-fraction-ℤ :
    sim-fraction-ℤ p q →
    le-fraction-ℤ q r →
    le-fraction-ℤ p r
  concatenate-sim-le-fraction-ℤ H H' =
    is-positive-right-factor-mul-ℤ
      ( is-positive-eq-ℤ
        ( lemma-left-sim-cross-mul-diff-fraction-ℤ p q r H)
        ( is-positive-mul-ℤ
          ( is-positive-denominator-fraction-ℤ p)
          ( H')))
      ( is-positive-denominator-fraction-ℤ q)

  concatenate-le-sim-fraction-ℤ :
    le-fraction-ℤ p q →
    sim-fraction-ℤ q r →
    le-fraction-ℤ p r
  concatenate-le-sim-fraction-ℤ H H' =
    is-positive-right-factor-mul-ℤ
      ( is-positive-eq-ℤ
        ( inv ( lemma-right-sim-cross-mul-diff-fraction-ℤ p q r H'))
        ( is-positive-mul-ℤ
          ( is-positive-denominator-fraction-ℤ r)
          ( H)))
      ( is-positive-denominator-fraction-ℤ q)

The similarity of integer fractions preserves strict inequality

module _
  (p q p' q' : fraction-ℤ) (H : sim-fraction-ℤ p p') (K : sim-fraction-ℤ q q')
  where

  preserves-le-sim-fraction-ℤ : le-fraction-ℤ p q → le-fraction-ℤ p' q'
  preserves-le-sim-fraction-ℤ I =
    concatenate-sim-le-fraction-ℤ p' p q'
      ( symmetric-sim-fraction-ℤ p p' H)
      ( concatenate-le-sim-fraction-ℤ p q q' I K)

Fractions with equal denominator compare the same as their numerators

module _
  (x y : fraction-ℤ) (H : denominator-fraction-ℤ x ＝ denominator-fraction-ℤ y)
  where

  le-fraction-le-numerator-fraction-ℤ :
    le-ℤ (numerator-fraction-ℤ x) (numerator-fraction-ℤ y) →
    le-fraction-ℤ x y
  le-fraction-le-numerator-fraction-ℤ H' =
    tr
      ( λ (k : ℤ) →
        le-ℤ
          ( numerator-fraction-ℤ x *ℤ k)
          ( numerator-fraction-ℤ y *ℤ denominator-fraction-ℤ x))
      ( H)
      ( preserves-le-left-mul-positive-ℤ
        ( positive-denominator-fraction-ℤ x)
        ( numerator-fraction-ℤ x)
        ( numerator-fraction-ℤ y)
        ( H'))

The mediant of two distinct fractions lies strictly between them

module _
  (x y : fraction-ℤ)
  where

  le-left-mediant-fraction-ℤ :
    le-fraction-ℤ x y →
    le-fraction-ℤ x (mediant-fraction-ℤ x y)
  le-left-mediant-fraction-ℤ =
    is-positive-eq-ℤ (cross-mul-diff-left-mediant-fraction-ℤ x y)

  le-right-mediant-fraction-ℤ :
    le-fraction-ℤ x y →
    le-fraction-ℤ (mediant-fraction-ℤ x y) y
  le-right-mediant-fraction-ℤ =
    is-positive-eq-ℤ (cross-mul-diff-right-mediant-fraction-ℤ x y)

Strict inequality on the integer fractions is dense

module _
  (x y : fraction-ℤ) (H : le-fraction-ℤ x y)
  where

  dense-le-fraction-ℤ :
    exists fraction-ℤ (λ r → le-fraction-ℤ-Prop x r ∧ le-fraction-ℤ-Prop r y)
  dense-le-fraction-ℤ =
    intro-exists
      ( mediant-fraction-ℤ x y)
      ( le-left-mediant-fraction-ℤ x y H , le-right-mediant-fraction-ℤ x y H)

Strict inequality on the integer fractions is located

module _
  (x y z : fraction-ℤ)
  where

  located-le-fraction-ℤ :
    le-fraction-ℤ y z →
    type-disjunction-Prop (le-fraction-ℤ-Prop y x) (le-fraction-ℤ-Prop x z)
  located-le-fraction-ℤ H =
    unit-trunc-Prop
      ( map-coproduct
        ( id)
        ( λ p → concatenate-leq-le-fraction-ℤ x y z p H)
        ( decide-le-leq-fraction-ℤ y x))

x < y if and only if 0 < y - x

module _
  (x y : fraction-ℤ)
  where

  eq-translate-diff-le-zero-fraction-ℤ :
    le-fraction-ℤ zero-fraction-ℤ (y +fraction-ℤ (neg-fraction-ℤ x)) ＝
    le-fraction-ℤ x y
  eq-translate-diff-le-zero-fraction-ℤ =
    ap
      ( is-positive-ℤ)
      ( ( cross-mul-diff-zero-fraction-ℤ (y +fraction-ℤ (neg-fraction-ℤ x))) ∙
        ( ap
          ( add-ℤ ( (numerator-fraction-ℤ y) *ℤ (denominator-fraction-ℤ x)))
          ( left-negative-law-mul-ℤ
            ( numerator-fraction-ℤ x)
            ( denominator-fraction-ℤ y))))

Recent changes