Addition on nonnegative rational numbers

Content created by Louis Wasserman.

Created on 2025-10-03.
Last modified on 2025-10-03.

module elementary-number-theory.addition-nonnegative-rational-numbers where
Imports 
open import elementary-number-theory.addition-rational-numbers
open import elementary-number-theory.inequality-rational-numbers
open import elementary-number-theory.nonnegative-integer-fractions
open import elementary-number-theory.nonnegative-rational-numbers
open import elementary-number-theory.rational-numbers

open import foundation.dependent-pair-types
open import foundation.transport-along-identifications

open import order-theory.inflationary-maps-posets

Idea

The sum of two nonnegative rational numbers is their sum as rational numbers, and is itself nonnegative.

Definition

opaque
  unfolding add-ℚ

  is-nonnegative-add-ℚ :
    (p q : ℚ) → is-nonnegative-ℚ p → is-nonnegative-ℚ q →
    is-nonnegative-ℚ (p +ℚ q)
  is-nonnegative-add-ℚ p q nonneg-p nonneg-q =
    is-nonnegative-rational-fraction-ℤ
      ( is-nonnegative-add-fraction-ℤ
        { fraction-ℚ p}
        { fraction-ℚ q}
        ( nonneg-p)
        ( nonneg-q))

add-ℚ⁰⁺ : ℚ⁰⁺ → ℚ⁰⁺ → ℚ⁰⁺
add-ℚ⁰⁺ (p , nonneg-p) (q , nonneg-q) =
  ( p +ℚ q , is-nonnegative-add-ℚ p q nonneg-p nonneg-q)

infixl 35 _+ℚ⁰⁺_
_+ℚ⁰⁺_ : ℚ⁰⁺ → ℚ⁰⁺ → ℚ⁰⁺
_+ℚ⁰⁺_ = add-ℚ⁰⁺

Properties

Addition of a nonnegative rational number is an increasing map

abstract
  is-inflationary-map-left-add-rational-ℚ⁰⁺ :
    (p : ℚ⁰⁺) → is-inflationary-map-Poset ℚ-Poset (rational-ℚ⁰⁺ p +ℚ_)
  is-inflationary-map-left-add-rational-ℚ⁰⁺ (p , nonneg-p) q =
    tr
      ( λ r → leq-ℚ r (p +ℚ q))
      ( left-unit-law-add-ℚ q)
      ( preserves-leq-left-add-ℚ
        ( q)
        ( zero-ℚ)
        ( p)
        ( leq-zero-is-nonnegative-ℚ p nonneg-p))

  is-inflationary-map-right-add-rational-ℚ⁰⁺ :
    (p : ℚ⁰⁺) → is-inflationary-map-Poset ℚ-Poset (_+ℚ rational-ℚ⁰⁺ p)
  is-inflationary-map-right-add-rational-ℚ⁰⁺ p q =
    tr
      ( leq-ℚ q)
      ( commutative-add-ℚ (rational-ℚ⁰⁺ p) q)
      ( is-inflationary-map-left-add-rational-ℚ⁰⁺ p q)

Recent changes