# Positive integer fractions

Content created by Fredrik Bakke and malarbol.

Created on 2024-04-25.

module elementary-number-theory.positive-integer-fractions where

Imports
open import elementary-number-theory.addition-integer-fractions
open import elementary-number-theory.integer-fractions
open import elementary-number-theory.integers
open import elementary-number-theory.multiplication-integer-fractions
open import elementary-number-theory.multiplication-positive-and-negative-integers
open import elementary-number-theory.positive-integers
open import elementary-number-theory.reduced-integer-fractions

open import foundation.propositions
open import foundation.subtypes
open import foundation.universe-levels


## Idea

An integer fraction x is said to be positive if its numerator is a positive integer.

## Definitions

### The property of being a positive integer fraction

module _
(x : fraction-ℤ)
where

is-positive-fraction-ℤ : UU lzero
is-positive-fraction-ℤ = is-positive-ℤ (numerator-fraction-ℤ x)

is-prop-is-positive-fraction-ℤ : is-prop is-positive-fraction-ℤ
is-prop-is-positive-fraction-ℤ =
is-prop-is-positive-ℤ (numerator-fraction-ℤ x)


## Properties

### An integer fraction similar to a positive integer fraction is positive

is-positive-sim-fraction-ℤ :
(x y : fraction-ℤ) (S : sim-fraction-ℤ x y) →
is-positive-fraction-ℤ x →
is-positive-fraction-ℤ y
is-positive-sim-fraction-ℤ x y S P =
is-positive-left-factor-mul-ℤ
( is-positive-eq-ℤ
( S)
( is-positive-mul-ℤ P (is-positive-denominator-fraction-ℤ y)))
( is-positive-denominator-fraction-ℤ x)


### The reduced fraction of a positive integer fraction is positive

is-positive-reduce-fraction-ℤ :
{x : fraction-ℤ} (P : is-positive-fraction-ℤ x) →
is-positive-fraction-ℤ (reduce-fraction-ℤ x)
is-positive-reduce-fraction-ℤ {x} =
is-positive-sim-fraction-ℤ
( x)
( reduce-fraction-ℤ x)
( sim-reduced-fraction-ℤ x)


### The sum of two positive integer fractions is positive

is-positive-add-fraction-ℤ :
{x y : fraction-ℤ} →
is-positive-fraction-ℤ x →
is-positive-fraction-ℤ y →
is-positive-add-fraction-ℤ {x} {y} P Q =
( is-positive-mul-ℤ P (is-positive-denominator-fraction-ℤ y))
( is-positive-mul-ℤ Q (is-positive-denominator-fraction-ℤ x))


### The product of two positive integer fractions is positive

is-positive-mul-fraction-ℤ :
{x y : fraction-ℤ} →
is-positive-fraction-ℤ x →
is-positive-fraction-ℤ y →
is-positive-fraction-ℤ (mul-fraction-ℤ x y)
is-positive-mul-fraction-ℤ {x} {y} = is-positive-mul-ℤ