Translation preserves strict inequality on natural numbers (#1254)

Function names etc. adapted from the analogous results proved for the
integers.

CONTRIBUTORS.toml

@@ -252,3 +252,8 @@ github = "djspacewhale"
 displayName = "Job Petrovčič"
 usernames = [ "Job Petrovčič", "JobPetrovcic" ]
 github = "JobPetrovcic"
+
+[[contributors]]
+displayName = "Louis Wasserman"
+usernames = [ "Louis Wasserman" ]
+github = "lowasser"

src/elementary-number-theory/strict-inequality-natural-numbers.lagda.md

@@ -12,7 +12,9 @@ open import elementary-number-theory.inequality-natural-numbers
 open import elementary-number-theory.multiplication-natural-numbers
 open import elementary-number-theory.natural-numbers
 
+open import foundation.action-on-identifications-binary-functions
 open import foundation.action-on-identifications-functions
+open import foundation.binary-transport
 open import foundation.cartesian-product-types
 open import foundation.coproduct-types
 open import foundation.decidable-types
@@ -324,3 +326,42 @@ le-leq-neq-ℕ {succ-ℕ x} {succ-ℕ y} l f =
 le-one-mul-ℕ : (x y : ℕ) → 1 <-ℕ x → 1 <-ℕ y → 1 <-ℕ (x *ℕ y)
 le-one-mul-ℕ (succ-ℕ (succ-ℕ x)) (succ-ℕ (succ-ℕ y)) star star = star
 ```
+
+### Strict inequality on the natural numbers is invariant by translation
+
+```agda
+eq-translate-right-le-ℕ : (z x y : ℕ) → le-ℕ (x +ℕ z) (y +ℕ z) ＝ le-ℕ x y
+eq-translate-right-le-ℕ zero-ℕ x y = refl
+eq-translate-right-le-ℕ (succ-ℕ z) x y = eq-translate-right-le-ℕ z x y
+
+eq-translate-left-le-ℕ : (z x y : ℕ) → le-ℕ (z +ℕ x) (z +ℕ y) ＝ le-ℕ x y
+eq-translate-left-le-ℕ z x y =
+  ap-binary le-ℕ (commutative-add-ℕ z x) (commutative-add-ℕ z y) ∙
+  eq-translate-right-le-ℕ z x y
+```
+
+### Addition on the natural numbers preserves strict inequality
+
+```agda
+preserves-le-right-add-ℕ : (z x y : ℕ) → le-ℕ x y → le-ℕ (x +ℕ z) (y +ℕ z)
+preserves-le-right-add-ℕ zero-ℕ x y I = I
+preserves-le-right-add-ℕ (succ-ℕ z) x y I = preserves-le-right-add-ℕ z x y I
+
+preserves-le-left-add-ℕ : (z x y : ℕ) → le-ℕ x y → le-ℕ (z +ℕ x) (z +ℕ y)
+preserves-le-left-add-ℕ z x y I =
+  binary-tr
+    le-ℕ
+    (commutative-add-ℕ x z)
+    (commutative-add-ℕ y z)
+    (preserves-le-right-add-ℕ z x y I)
+
+preserves-le-add-ℕ :
+  {a b c d : ℕ} → le-ℕ a b → le-ℕ c d → le-ℕ (a +ℕ c) (b +ℕ d)
+preserves-le-add-ℕ {a} {b} {c} {d} H K =
+  transitive-le-ℕ
+    (a +ℕ c)
+    (b +ℕ c)
+    (b +ℕ d)
+    (preserves-le-right-add-ℕ c a b H)
+    (preserves-le-left-add-ℕ b c d K)
+```