Inequality on integer fractions

Content created by Fredrik Bakke, malarbol, Egbert Rijke and Fernando Chu.

Created on 2023-04-08.
Last modified on 2024-04-09.

module elementary-number-theory.inequality-integer-fractions where
Imports 
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-integers
open import elementary-number-theory.integer-fractions
open import elementary-number-theory.integers
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.coproduct-types
open import foundation.decidable-propositions
open import foundation.dependent-pair-types
open import foundation.function-types
open import foundation.identity-types
open import foundation.negation
open import foundation.propositions
open import foundation.transport-along-identifications
open import foundation.universe-levels

Idea

An integer fraction m/n is less or equal to a fraction m'/n' if the integer product m * n' is less or equal to m' * n.

Definition

Inequality on integer fractions

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

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

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

Properties

Inequality on integer fractions is decidable

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

leq-fraction-ℤ-Decidable-Prop : (x y : fraction-ℤ) → Decidable-Prop lzero
leq-fraction-ℤ-Decidable-Prop x y =
  ( leq-fraction-ℤ x y ,
    is-prop-leq-fraction-ℤ x y ,
    is-decidable-leq-fraction-ℤ x y)

Inequality on integer fractions is antisymmetric with respect to the similarity relation

module _
  (x y : fraction-ℤ)
  where

  is-sim-antisymmetric-leq-fraction-ℤ :
    leq-fraction-ℤ x y →
    leq-fraction-ℤ y x →
    sim-fraction-ℤ x y
  is-sim-antisymmetric-leq-fraction-ℤ H H' =
    sim-is-zero-coss-mul-diff-fraction-ℤ x y
      ( is-zero-is-nonnegative-is-nonpositive-ℤ
        ( H)
        ( is-nonpositive-eq-ℤ
          ( skew-commutative-cross-mul-diff-fraction-ℤ y x)
          ( is-nonpositive-neg-is-nonnegative-ℤ
            ( H'))))

Inequality on integer fractions is transitive

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

Recent changes