Solver for equations over ℚ

src/1Lab/HLevel/Closure.lagda.md

@@ -188,6 +188,14 @@ between functions is a function into identities:
   (λ f {x} → f x) (λ f x → f) (λ _ → refl)
   (Π-is-hlevel n bhl)
 
+Π-is-hlevel-inst
+  : ∀ {a b} {A : Type a} {B : A → Type b}
+  → (n : Nat) (Bhl : (x : A) → is-hlevel (B x) n)
+  → is-hlevel (⦃ x : A ⦄ → B x) n
+Π-is-hlevel-inst n bhl = retract→is-hlevel n
+  (λ f ⦃ x ⦄ → f x) (λ f x → f ⦃ x ⦄) (λ _ → refl)
+  (Π-is-hlevel n bhl)
+
 Π-is-hlevel²
   : ∀ {a b c} {A : Type a} {B : A → Type b} {C : ∀ a → B a → Type c}
   → (n : Nat) (Bhl : (x : A) (y : B x) → is-hlevel (C x y) n)
@@ -376,6 +384,12 @@ instance opaque
     → H-Level (∀ {x} → S x) n
   H-Level-pi' {n = n} .H-Level.has-hlevel = Π-is-hlevel' n λ _ → hlevel n
 
+  H-Level-pi''
+    : ∀ {n} {S : T → Type ℓ}
+    → ⦃ ∀ {x} → H-Level (S x) n ⦄
+    → H-Level (∀ ⦃ x ⦄ → S x) n
+  H-Level-pi'' {n = n} .H-Level.has-hlevel = Π-is-hlevel-inst n λ _ → hlevel n
+
   H-Level-sigma
     : ∀ {n} {S : T → Type ℓ}
     → ⦃ H-Level T n ⦄ → ⦃ ∀ {x} → H-Level (S x) n ⦄

src/Algebra/Group/Instances/Integers.lagda.md

@@ -9,7 +9,7 @@ open import Cat.Prelude
 
 open import Data.Int.Universal
 open import Data.Nat.Order
-open import Data.Int hiding (Positive)
+open import Data.Int hiding (Positive ; <-not-equal)
 open import Data.Nat
 
 open is-group-hom

src/Algebra/Ring/Solver.agda

@@ -46,10 +46,15 @@ module Impl {ℓ} {R : Type ℓ} (cring : CRing-on R) where
 
     ℤ↪R-rh = Int-is-initial R' .centre
     module ℤ↪R = is-ring-hom (ℤ↪R-rh .preserves)
-    embed-coe = ℤ↪R-rh .hom
 
     open CRing-on cring using (*-commutes)
 
+  embed-coe : Int → R
+  embed-coe x = ℤ↪R-rh .hom (lift x)
+
+  embed-lemma : {h' : Int → R} → is-ring-hom (Liftℤ {ℓ} .snd) (R' .snd) (h' ⊙ lower) → ∀ x → embed-coe x ≡ h' x
+  embed-lemma p x = happly (ap Total-hom.hom (Int-is-initial R' .paths (total-hom _ p))) (lift x)
+
   data Poly   : Nat → Type ℓ
   data Normal : Nat → Type ℓ
 
@@ -67,7 +72,7 @@ module Impl {ℓ} {R : Type ℓ} (cring : CRing-on R) where
   Ep ∅ i = R.0r
   Ep (p *x+ c) (x ∷ e) = Ep p (x ∷ e) R.* x R.+ En c e
 
-  En (con x) i = embed-coe (lift x)
+  En (con x) i = embed-coe x
   En (poly x) i = Ep x i
 
   0h : ∀ {n} → Poly n
@@ -200,7 +205,7 @@ module Impl {ℓ} {R : Type ℓ} (cring : CRing-on R) where
     Number-Polynomial .Number.fromNat n = con (pos n)
 
   eval (op o p₁ p₂) ρ = sem o (⟦ p₁ ⟧ ρ) (⟦ p₂ ⟧ ρ)
-  eval (con c)      ρ = embed-coe (lift c)
+  eval (con c)      ρ = embed-coe c
   eval (var x)      ρ = lookup ρ x
   eval (:- p)       ρ = R.- ⟦ p ⟧ ρ
 
@@ -371,7 +376,7 @@ module Impl {ℓ} {R : Type ℓ} (cring : CRing-on R) where
   -ₙ-hom (poly x) ρ = -ₚ-hom x ρ
 
   sound-coe
-    : ∀ {n} (c : Int) (ρ : Vec R n) → En (normal-coe c) ρ ≡ embed-coe (lift c)
+    : ∀ {n} (c : Int) (ρ : Vec R n) → En (normal-coe c) ρ ≡ embed-coe c
   sound-coe c [] = refl
   sound-coe c (x ∷ ρ) = ∅*x+ₙ-hom (normal-coe c) x ρ ∙ sound-coe c ρ
 

src/Data/Fin/Product.lagda.md

@@ -193,6 +193,23 @@ curry-∀ᶠ
   → ∀ᶠ n P Q
 curry-∀ᶠ {zero} f = f tt
 curry-∀ᶠ {suc n} f a = curry-∀ᶠ {n} λ b → f (a , b)
+
+∀ᶠⁱ : ∀ n {ℓ ℓ'} (P : (i : Fin n) → Type (ℓ i)) (Q : Πᶠ P → Type ℓ') → Type (ℓ-maxᶠ ℓ ⊔ ℓ')
+∀ᶠⁱ zero P Q = Q tt
+∀ᶠⁱ (suc n) P Q = {a : P fzero} → ∀ᶠⁱ n (λ i → P (fsuc i)) (λ b → Q (a , b))
+
+apply-∀ᶠⁱ
+  : ∀ {n} {ℓ : Fin n → Level} {ℓ'} {P : (i : Fin n) → Type (ℓ i)} {Q : Πᶠ P → Type ℓ'}
+  → ∀ᶠⁱ n P Q → (a : Πᶠ P) → Q a
+apply-∀ᶠⁱ {zero} f a = f
+apply-∀ᶠⁱ {suc n} f (a , as) = apply-∀ᶠⁱ (f {a}) as
+
+curry-∀ᶠⁱ
+  : ∀ {n} {ℓ : Fin n → Level} {ℓ'} {P : (i : Fin n) → Type (ℓ i)} {Q : Πᶠ P → Type ℓ'}
+  → ((a : Πᶠ P) → Q a)
+  → ∀ᶠⁱ n P Q
+curry-∀ᶠⁱ {zero} f = f tt
+curry-∀ᶠⁱ {suc n} f {a} = curry-∀ᶠⁱ {n} λ b → f (a , b)
 ```
 -->
 

src/Data/Int/DivMod.lagda.md

@@ -10,7 +10,7 @@ open import Data.Int.Divisible
 open import Data.Nat.DivMod
 open import Data.Dec.Base
 open import Data.Fin hiding (_<_)
-open import Data.Int hiding (Positive)
+open import Data.Int hiding (Positive ; _<_ ; <-weaken)
 open import Data.Nat as Nat
 ```
 -->

src/Data/Int/Order.lagda.md

@@ -7,6 +7,7 @@ open import 1Lab.Type
 
 open import Data.Int.Properties
 open import Data.Int.Base
+open import Data.Sum.Base
 open import Data.Dec
 
 import Data.Nat.Properties as Nat
@@ -33,6 +34,20 @@ data _≤_ : Int → Int → Type where
   neg≤pos : ∀ {x y}             → negsuc x ≤ pos y
 ```
 
+<!--
+```agda
+instance
+  ≤-neg-neg : ∀ {x y} ⦃ p : y Nat.≤ x ⦄ → negsuc x ≤ negsuc y
+  ≤-neg-neg ⦃ p ⦄ = neg≤neg p
+
+  ≤-pos-pos : ∀ {x y} ⦃ p : x Nat.≤ y ⦄ → pos x ≤ pos y
+  ≤-pos-pos ⦃ p ⦄ = pos≤pos p
+
+  ≤-neg-pos : ∀ {x y} → negsuc x ≤ pos y
+  ≤-neg-pos = neg≤pos
+```
+-->
+
 Note the key properties: the ordering between negative numbers is
 reversed, and every negative number is smaller than every positive
 number.  This means that $\bZ$ decomposes, as an order, into an _ordinal
@@ -245,4 +260,192 @@ abstract
 
   *ℤ-nonnegative : ∀ {x y} → 0 ≤ x → 0 ≤ y → 0 ≤ (x *ℤ y)
   *ℤ-nonnegative {pos x} {pos y} (pos≤pos p) (pos≤pos q) = ≤-trans (pos≤pos Nat.0≤x) (≤-refl' (sym (assign-pos (x * y))))
+
+  positive→nonnegative : ∀ {x} → Positive x → 0 ≤ x
+  positive→nonnegative (pos x) = pos≤pos Nat.0≤x
+
+  -ℕ-nonnegative : ∀ {x y} → y Nat.≤ x → 0 ≤ (x ℕ- y)
+  -ℕ-nonnegative {x} {y} Nat.0≤x = pos≤pos Nat.0≤x
+  -ℕ-nonnegative {suc x} {suc y} (Nat.s≤s p) = -ℕ-nonnegative p
+
+  -ℤ-nonnegative : ∀ {x y} → 0 ≤ x → 0 ≤ y → y ≤ x → 0 ≤ (x -ℤ y)
+  -ℤ-nonnegative {posz} {posz} (pos≤pos p) (pos≤pos q) (pos≤pos r) = pos≤pos Nat.0≤x
+  -ℤ-nonnegative {possuc x} {posz} (pos≤pos p) (pos≤pos q) (pos≤pos r) = pos≤pos Nat.0≤x
+  -ℤ-nonnegative {possuc x} {possuc y} (pos≤pos p) (pos≤pos q) (pos≤pos r) = -ℕ-nonnegative (Nat.≤-peel r)
+```
+
+# The strict order
+
+```agda
+data _<_ : Int → Int → Type where
+  pos<pos : ∀ {x y} → x Nat.< y → pos x < pos y
+  neg<pos : ∀ {x y} → negsuc x < pos y
+  neg<neg : ∀ {x y} → y Nat.< x → negsuc x < negsuc y
+
+instance
+  H-Level-< : ∀ {x y n} → H-Level (x < y) (suc n)
+  H-Level-< = prop-instance λ where
+    (pos<pos x) (pos<pos y) → ap pos<pos (Nat.≤-is-prop x y)
+    neg<pos neg<pos → refl
+    (neg<neg x) (neg<neg y) → ap neg<neg (Nat.≤-is-prop x y)
+
+<-not-equal : ∀ {x y} → x < y → x ≠ y
+<-not-equal (pos<pos p) q = Nat.<-not-equal p (pos-injective q)
+<-not-equal neg<pos q = negsuc≠pos q
+<-not-equal (neg<neg p) q = Nat.<-not-equal p (negsuc-injective (sym q))
+
+<-irrefl : ∀ {x y} → x ≡ y → ¬ (x < y)
+<-irrefl p q = <-not-equal q p
+
+<-weaken : ∀ {x y} → x < y → x ≤ y
+<-weaken (pos<pos x) = pos≤pos (Nat.<-weaken x)
+<-weaken neg<pos = neg≤pos
+<-weaken (neg<neg x) = neg≤neg (Nat.<-weaken x)
+
+<-asym : ∀ {x y} → x < y → ¬ (y < x)
+<-asym (pos<pos x) (pos<pos y) = Nat.<-asym x y
+<-asym (neg<neg x) (neg<neg y) = Nat.<-asym x y
+
+≤-strengthen : ∀ {x y} → x ≤ y → (x ≡ y) ⊎ (x < y)
+≤-strengthen (neg≤neg x) with Nat.≤-strengthen x
+... | inl x=y = inl (ap negsuc (sym x=y))
+... | inr x<y = inr (neg<neg x<y)
+≤-strengthen (pos≤pos x) with Nat.≤-strengthen x
+... | inl x=y = inl (ap pos x=y)
+... | inr x<y = inr (pos<pos x<y)
+≤-strengthen neg≤pos = inr neg<pos
+
+<-from-≤ : ∀ {x y} → x ≤ y → x ≠ y → x < y
+<-from-≤ x≤y x≠y with ≤-strengthen x≤y
+... | inl x=y = absurd (x≠y x=y)
+... | inr p = p
+
+<-dec : ∀ x y → Dec (x < y)
+<-dec (pos x) (pos y) with Nat.≤-dec (suc x) y
+... | yes x<y = yes (pos<pos x<y)
+... | no ¬x<y = no λ { (pos<pos x<y) → ¬x<y x<y }
+<-dec (pos x) (negsuc y) = no λ ()
+<-dec (negsuc x) (pos y) = yes neg<pos
+<-dec (negsuc x) (negsuc y) with Nat.≤-dec (suc y) x
+... | yes y<x = yes (neg<neg y<x)
+... | no ¬y<x = no λ { (neg<neg y<x) → ¬y<x y<x }
+
+instance
+  Dec-< : ∀ {x y} → Dec (x < y)
+  Dec-< {x} {y} = <-dec x y
+
+≤-from-not-< : ∀ {x y} → ¬ x < y → y ≤ x
+≤-from-not-< {pos x} {pos y} ¬x<y = pos≤pos (Nat.≤-from-not-< x y (λ x<y → ¬x<y (pos<pos x<y)))
+≤-from-not-< {pos x} {negsuc y} ¬x<y = neg≤pos
+≤-from-not-< {negsuc x} {pos y} ¬x<y = absurd (¬x<y neg<pos)
+≤-from-not-< {negsuc x} {negsuc y} ¬x<y = neg≤neg (Nat.≤-from-not-< y x (λ y<x → ¬x<y (neg<neg y<x)))
+
+<-linear : ∀ {x y} → ¬ x < y → ¬ y < x → x ≡ y
+<-linear {x} {y} ¬x<y ¬y<x = ≤-antisym (≤-from-not-< ¬y<x) (≤-from-not-< ¬x<y)
+
+<-split : ∀ x y → (x < y) ⊎ (x ≡ y) ⊎ (y < x)
+<-split x y with <-dec x y
+... | yes x<y = inl x<y
+... | no ¬x<y with <-dec y x
+... | yes y<x = inr (inr y<x)
+... | no ¬y<x = inr (inl (<-linear ¬x<y ¬y<x))
+
+<-trans : ∀ {x y z} → x < y → y < z → x < z
+<-trans (pos<pos p) (pos<pos q) = pos<pos (Nat.<-trans _ _ _ p q)
+<-trans neg<pos (pos<pos q) = neg<pos
+<-trans (neg<neg p) neg<pos = neg<pos
+<-trans (neg<neg p) (neg<neg q) = neg<neg (Nat.<-trans _ _ _ q p)
+
+<-≤-trans : ∀ {x y z} → x < y → y ≤ z → x < z
+<-≤-trans p q with ≤-strengthen q
+... | inl y=z = subst₂ _<_ refl y=z p
+... | inr y<z = <-trans p y<z
+
+≤-<-trans : ∀ {x y z} → x ≤ y → y < z → x < z
+≤-<-trans p q with ≤-strengthen p
+... | inl x=y = subst₂ _<_ (sym x=y) refl q
+... | inr x<y = <-trans x<y q
+
+abstract
+  nat-diff-<-possuc : ∀ k x → (k ℕ- x) < possuc k
+  nat-diff-<-possuc zero zero = pos<pos (Nat.s≤s Nat.0≤x)
+  nat-diff-<-possuc zero (suc x) = neg<pos
+  nat-diff-<-possuc (suc k) zero = pos<pos Nat.≤-refl
+  nat-diff-<-possuc (suc k) (suc x) = <-trans (nat-diff-<-possuc k x) (pos<pos Nat.≤-refl)
+
+  nat-diff-<-pos : ∀ k x → (k ℕ- suc x) < pos k
+  nat-diff-<-pos zero zero = neg<pos
+  nat-diff-<-pos zero (suc x) = neg<pos
+  nat-diff-<-pos (suc k) zero = pos<pos auto
+  nat-diff-<-pos (suc k) (suc x) = nat-diff-<-possuc k (suc x)
+
+  negsuc-<-nat-diff : ∀ k x → negsuc k < (x ℕ- k)
+  negsuc-<-nat-diff zero zero = neg<pos
+  negsuc-<-nat-diff zero (suc x) = neg<pos
+  negsuc-<-nat-diff (suc k) zero = neg<neg auto
+  negsuc-<-nat-diff (suc k) (suc x) = <-trans (neg<neg auto) (negsuc-<-nat-diff k x)
+
+  negsuc-≤-nat-diff : ∀ k x → negsuc k ≤ (x ℕ- suc k)
+  negsuc-≤-nat-diff zero zero = neg≤neg Nat.0≤x
+  negsuc-≤-nat-diff zero (suc x) = neg≤pos
+  negsuc-≤-nat-diff (suc k) zero = neg≤neg auto
+  negsuc-≤-nat-diff (suc k) (suc x) = ≤-trans (neg≤neg Nat.≤-ascend) (negsuc-≤-nat-diff k x)
+
+  nat-diff-preserves-<r : ∀ k {x y} → y Nat.< x → (k ℕ- x) < (k ℕ- y)
+  nat-diff-preserves-<r zero {suc zero} {zero} (Nat.s≤s Nat.0≤x) = neg<pos
+  nat-diff-preserves-<r zero {suc (suc x)} {zero} (Nat.s≤s p) = neg<pos
+  nat-diff-preserves-<r zero {suc (suc x)} {suc y} (Nat.s≤s p) = neg<neg p
+  nat-diff-preserves-<r (suc k) {suc x} {zero} (Nat.s≤s p) = nat-diff-<-possuc k x
+  nat-diff-preserves-<r (suc k) {suc x} {suc y} (Nat.s≤s p) = nat-diff-preserves-<r k {x} {y} p
+
+  nat-diff-preserves-<l : ∀ k {x y} → x Nat.< y → (x ℕ- k) < (y ℕ- k)
+  nat-diff-preserves-<l zero {zero} {suc y} (Nat.s≤s p) = pos<pos (Nat.s≤s Nat.0≤x)
+  nat-diff-preserves-<l zero {suc x} {suc y} (Nat.s≤s p) = pos<pos (Nat.s≤s p)
+  nat-diff-preserves-<l (suc k) {zero} {suc y} (Nat.s≤s Nat.0≤x) = negsuc-<-nat-diff k y
+  nat-diff-preserves-<l (suc k) {suc x} {suc y} (Nat.s≤s p) = nat-diff-preserves-<l k {x} {y} p
+
+  +ℤ-preserves-<r : ∀ x y z → x < y → (x +ℤ z) < (y +ℤ z)
+  +ℤ-preserves-<r x y (pos z) (pos<pos p) = pos<pos (Nat.+-preserves-<r _ _ z p)
+  +ℤ-preserves-<r (negsuc x) (pos y) (pos z) neg<pos =
+    let
+      rem₁ : z Nat.≤ y + z
+      rem₁ = Nat.≤-trans (Nat.+-≤l z y) (Nat.≤-refl' (Nat.+-commutative z y))
+    in <-≤-trans (nat-diff-<-pos z x) (pos≤pos rem₁)
+  +ℤ-preserves-<r x y (pos z) (neg<neg p) = nat-diff-preserves-<r z (Nat.s≤s p)
+  +ℤ-preserves-<r x y (negsuc z) (pos<pos p) = nat-diff-preserves-<l (suc z) p
+  +ℤ-preserves-<r (negsuc x) (pos y) (negsuc z) neg<pos =
+    let
+      rem₁ : suc z Nat.≤ suc (x + z)
+      rem₁ = Nat.≤-trans (Nat.+-≤l (suc z) x) (Nat.≤-refl' (ap suc (Nat.+-commutative z x)))
+    in <-≤-trans (neg<neg rem₁) (negsuc-≤-nat-diff z y)
+  +ℤ-preserves-<r x y (negsuc z) (neg<neg p) = neg<neg (Nat.s≤s (Nat.+-preserves-<r _ _ z p))
+
+  +ℤ-preserves-<l : ∀ x y z → x < y → (z +ℤ x) < (z +ℤ y)
+  +ℤ-preserves-<l x y z p = subst₂ _<_ (+ℤ-commutative x z) (+ℤ-commutative y z) (+ℤ-preserves-<r x y z p)
+
+  +ℤ-preserves-< : ∀ x y x' y' → x < y → x' < y' → (x +ℤ x') < (y +ℤ y')
+  +ℤ-preserves-< x y x' y' p q = <-trans (+ℤ-preserves-<r x y x' p) (+ℤ-preserves-<l x' y' y q)
+
+  *ℤ-cancel-<r : ∀ {x y z} ⦃ _ : Positive x ⦄ → (y *ℤ x) < (z *ℤ x) → y < z
+  *ℤ-cancel-<r {x} {y} {z} yx<zx = <-from-≤
+    (*ℤ-cancel-≤r {x} {y} {z} (<-weaken yx<zx))
+    λ y=z → <-irrefl (ap (_*ℤ x) y=z) yx<zx
+
+  *ℤ-cancel-<l : ∀ {x y z} ⦃ _ : Positive x ⦄ → (x *ℤ y) < (x *ℤ z) → y < z
+  *ℤ-cancel-<l {x} {y} {z} xy<xz = *ℤ-cancel-<r {x} {y} {z} (subst₂ _<_ (*ℤ-commutative x y) (*ℤ-commutative x z) xy<xz)
+
+  *ℤ-preserves-<r : ∀ {x y} z ⦃ _ : Positive z ⦄ → x < y → (x *ℤ z) < (y *ℤ z)
+  *ℤ-preserves-<r {x} {y} z x<y = <-from-≤
+    (*ℤ-preserves-≤r {x} {y} z (<-weaken x<y))
+    λ xz=yz → <-irrefl (*ℤ-injectiver z x y (positive→nonzero auto) xz=yz) x<y
+
+  negℤ-anti-< : ∀ {x y} → x < y → negℤ y < negℤ x
+  negℤ-anti-< {posz} {pos y} (pos<pos (Nat.s≤s p)) = neg<pos
+  negℤ-anti-< {possuc x} {pos y} (pos<pos (Nat.s≤s p)) = neg<neg p
+  negℤ-anti-< {negsuc x} {posz} neg<pos = pos<pos (Nat.s≤s Nat.0≤x)
+  negℤ-anti-< {negsuc x} {possuc y} neg<pos = neg<pos
+  negℤ-anti-< {negsuc x} {negsuc y} (neg<neg p) = pos<pos (Nat.s≤s p)
+
+  negℤ-anti-full-< : ∀ {x y} → negℤ x < negℤ y → y < x
+  negℤ-anti-full-< {x} {y} p = subst₂ _<_ (negℤ-negℤ y) (negℤ-negℤ x) (negℤ-anti-< p)
 ```

src/Data/Int/Properties.lagda.md

@@ -518,6 +518,11 @@ no further comments.
 *ℤ-positive : ∀ {x y} → Positive x → Positive y → Positive (x *ℤ y)
 *ℤ-positive (pos x) (pos y) = pos (y + x * suc y)
 
+*ℤ-nonzero : ∀ {x y} → x ≠ 0 → y ≠ 0 → (x *ℤ y) ≠ 0
+*ℤ-nonzero {x} {y} x≠0 y≠0 p with *ℤ-is-zero x y p
+... | inl x=0 = x≠0 x=0
+... | inr y=0 = y≠0 y=0
+
 +ℤ-positive : ∀ {x y} → Positive x → Positive y → Positive (x +ℤ y)
 +ℤ-positive (pos x) (pos y) = pos (x + suc y)
 
@@ -531,4 +536,7 @@ positive→nonzero .{possuc x} (pos x) p = suc≠zero (pos-injective p)
 *ℤ-positive-cancel : ∀ {x y} → Positive x → Positive (x *ℤ y) → Positive y
 *ℤ-positive-cancel {pos .(suc x)} {posz} (pos x) q = absurd (positive→nonzero q (ap (assign pos) (*-zeror x)))
 *ℤ-positive-cancel {pos .(suc x)} {possuc y} (pos x) q = pos y
+
+*ℤ-nonzero-cancel : ∀ {x y} → (x *ℤ y) ≠ 0 → x ≠ 0
+*ℤ-nonzero-cancel {x} {y} xy≠0 x=0 = absurd (xy≠0 (ap (_*ℤ y) x=0))
 ```

src/Data/Nat/Order.lagda.md

@@ -160,6 +160,15 @@ module _ where private
 <-from-not-≤ (suc x) (suc y) ¬s≤s = s≤s $
   <-from-not-≤ x y λ z → ¬s≤s (s≤s z)
 
+≤-from-not-< : ∀ x y → ¬ (x < y) → y ≤ x
+≤-from-not-< zero zero p = 0≤x
+≤-from-not-< zero (suc y) p = absurd (p (s≤s 0≤x))
+≤-from-not-< (suc x) zero p = 0≤x
+≤-from-not-< (suc x) (suc y) p = s≤s (≤-from-not-< x y (p ∘ s≤s))
+
+<-trans : ∀ x y z → x < y → y < z → x < z
+<-trans x (suc y) (suc z) (s≤s p) (s≤s q) = ≤-trans (s≤s p) (≤-trans q ≤-ascend)
+
 ≤-uncap : ∀ m n → m ≠ suc n → m ≤ suc n → m ≤ n
 ≤-uncap m n p 0≤x = 0≤x
 ≤-uncap (suc x) zero p (s≤s 0≤x) = absurd (p refl)

src/Data/Nat/Properties.lagda.md

@@ -235,6 +235,14 @@ monus-≤ (suc x) (suc y) = ≤-sucr (monus-≤ x y)
 +-preserves-≤ x y x' y' prf prf' = ≤-trans
   (+-preserves-≤r x y x' prf) (+-preserves-≤l x' y' y prf')
 
++-preserves-<l : (x y z : Nat) → x < y → (z + x) < (z + y)
++-preserves-<l x (suc y) z (s≤s p) = ≤-trans (s≤s (+-preserves-≤l x y z p)) (≤-refl' (sym (+-sucr z y)))
+
++-preserves-<r : (x y z : Nat) → x < y → (x + z) < (y + z)
++-preserves-<r x y z p = subst₂ _<_ (+-commutative z x) (+-commutative z y) (+-preserves-<l x y z p)
+
++-preserves-< : ∀ x y x' y' → x < y → x' < y' → (x + x') < (y + y')
++-preserves-< x y x' y' p q = <-trans _ _ _ (+-preserves-<r x y x' p) (+-preserves-<l x' y' y q)
 
 *-preserves-≤l : (x y z : Nat) → x ≤ y → (z * x) ≤ (z * y)
 *-preserves-≤l x y zero prf = 0≤x