# Addition on the rational numbers

Content created by Egbert Rijke, Fredrik Bakke, Julian KG, fernabnor and louismntnu.

Created on 2023-06-25.

{-# OPTIONS --lossy-unification #-}


Imports
open import elementary-number-theory.addition-integer-fractions
open import elementary-number-theory.integer-fractions
open import elementary-number-theory.rational-numbers
open import elementary-number-theory.reduced-integer-fractions

open import foundation.action-on-identifications-binary-functions
open import foundation.dependent-pair-types
open import foundation.identity-types


## Idea

We introduce addition on the rationals and derive its basic properties. Properties of addition with respect to inequality are derived in inequality-rationals.

## Definition

add-ℚ : ℚ → ℚ → ℚ
add-ℚ (x , p) (y , q) = in-fraction-ℤ (add-fraction-ℤ x y)

add-ℚ' : ℚ → ℚ → ℚ

infixl 35 _+ℚ_

{x y x' y' : ℚ} → x ＝ x' → y ＝ y' → x +ℚ y ＝ x' +ℚ y'


## Properties

### Unit laws

left-unit-law-add-ℚ : (x : ℚ) → zero-ℚ +ℚ x ＝ x
eq-ℚ-sim-fractions-ℤ
( x)
in-fraction-fraction-ℚ (x , p)

right-unit-law-add-ℚ : (x : ℚ) → x +ℚ zero-ℚ ＝ x
eq-ℚ-sim-fractions-ℤ
( x)
in-fraction-fraction-ℚ (x , p)


associative-add-ℚ :
(x y z : ℚ) →
(x +ℚ y) +ℚ z ＝ x +ℚ (y +ℚ z)
associative-add-ℚ (x , px) (y , py) (z , pz) =
equational-reasoning
by eq-ℚ-sim-fractions-ℤ _ _
( symmetric-sim-fraction-ℤ _ _
( refl-sim-fraction-ℤ z))
by eq-ℚ-sim-fractions-ℤ _ _ (associative-add-fraction-ℤ x y z)
＝ in-fraction-ℤ
by eq-ℚ-sim-fractions-ℤ _ _
( refl-sim-fraction-ℤ x)


commutative-add-ℚ :