-- The order of the integers: nonnegative integers, ≤, and <
-- Part of Cumulus, the Grace17 mathematics library.
-- Copyright (c) 2026 Grant Passmore.
-- Released under the Apache License 2.0. See LICENSE in the repository root.
-- Authors: Grant Passmore

module Grace.Cumulus.Int.Order
import Ring
import AbsoluteValue

predicate IntegerNonnegative (z : Set) := ∃ n ∈ ℕ, z = integerOfNat(n)
predicate IntegerPositive (z : Set) := ∃ n ∈ ℕ, z = integerOfNat(n + 1)

predicate integerLe (x y : Integer) := IntegerNonnegative(y - x)
notation infix 50 "≤" => integerLe for Integer
notation infix 50 "≥" => reverse integerLe for Integer

predicate integerLess (x y : Integer) := integerLe(x + 1, y)
notation infix 50 "<" => integerLess for Integer

theorem IntegerNonnegative.ofNat (n : Nat)
  shows IntegerNonnegative(integerOfNat(n))
proof
  witness n
  constructor
  . typecheck
  . rfl

theorem IntegerNonnegative.integer (z : Set)
  requires nonnegative : IntegerNonnegative(z)
  shows Integer(z)
proof
  obtain ⟨n, nMember, shape⟩ := nonnegative
  have nNat := nat.omega.backward with nMember
  rw shape
  exact integerOfNat.integer with *

theorem IntegerNonnegative.zero
  shows IntegerNonnegative(integerZero)
proof
  have value := IntegerNonnegative.ofNat at 0
  rw integerOfNat.zero at value
  exact value

theorem IntegerNonnegative.one
  shows IntegerNonnegative(integerOne)
proof
  have value := IntegerNonnegative.ofNat at 1
  unfold integerOne
  exact value

theorem IntegerNonnegative.add (x y : Integer)
  requires first : IntegerNonnegative(x)
  requires second : IntegerNonnegative(y)
  shows IntegerNonnegative(x + y)
proof
  obtain ⟨n, nMember, xShape⟩ := first
  obtain ⟨m, mMember, yShape⟩ := second
  have nNat := nat.omega.backward with nMember
  have mNat := nat.omega.backward with mMember
  have sum := integerOfNat.add at n, m
  rw [xShape, yShape, ← sum]
  exact IntegerNonnegative.ofNat with *

theorem IntegerNonnegative.mul (x y : Integer)
  requires first : IntegerNonnegative(x)
  requires second : IntegerNonnegative(y)
  shows IntegerNonnegative(x * y)
proof
  obtain ⟨n, nMember, xShape⟩ := first
  obtain ⟨m, mMember, yShape⟩ := second
  have nNat := nat.omega.backward with nMember
  have mNat := nat.omega.backward with mMember
  have product := integerMulValue.ofNat at n, m
  rw [xShape, yShape, product]
  exact IntegerNonnegative.ofNat with *

theorem IntegerNonnegative.negative_iff (n : Nat)
  shows IntegerNonnegative(integerNegativeOfNat(n)) ↔ n = 0
proof
  constructor
  . intro nonnegative
    obtain ⟨m, mMember, shape⟩ := nonnegative
    have mNat := nat.omega.backward with mMember
    symm at shape
    have both := integerOfNat.eq_negative with shape
    exact both.right
  . intro zero
    rw zero
    have same : integerNegativeOfNat(0) = integerOfNat(0)
      simp [integerNegativeOfNat, integerOfNat]
    rw same
    exact IntegerNonnegative.ofNat with *

theorem IntegerNonnegative.cases (z : Integer)
  shows IntegerNonnegative(z) ∨ IntegerNonnegative(-z)
proof
  obtain ⟨n, nNat, sign⟩ := Integer.signed_natural at z with *
  cases sign with positive | negative
  . left
    rw positive
    exact IntegerNonnegative.ofNat with *
  . right
    rw negative
    have flipped := integerNegativeOfNat.neg at n
    rw flipped
    exact IntegerNonnegative.ofNat with *

theorem IntegerNonnegative.exists_natural (z : Integer)
  requires nonnegative : IntegerNonnegative(z)
  shows ∃ n, Nat(n) ∧ z = integerOfNat(n)
proof
  obtain ⟨n, nMember, shape⟩ := nonnegative
  have nNat := nat.omega.backward with nMember
  exact ⟨n, nNat, shape⟩

theorem IntegerNonnegative.eq_zero (z : Integer)
  requires first : IntegerNonnegative(z)
  requires second : IntegerNonnegative(-z)
  shows z = 0
proof
  obtain ⟨n, nMember, zShape⟩ := first
  obtain ⟨m, mMember, negShape⟩ := second
  have nNat := nat.omega.backward with nMember
  have mNat := nat.omega.backward with mMember
  have cancel : z + (-z) = 0 by ring
  rw [negShape, zShape] at cancel
  have sum := integerOfNat.add at n, m
  rw [← sum, ← integerOfNat.zero] at cancel
  have sumZero := integerOfNat.injective with cancel
  have both := add.eq_zero with sumZero
  rw [zShape, both.left]
  exact integerOfNat.zero

theorem IntegerNonnegative.of_positive (z : Integer)
  requires positive : IntegerPositive(z)
  shows IntegerNonnegative(z)
proof
  obtain ⟨n, nMember, shape⟩ := positive
  have nNat := nat.omega.backward with nMember
  rw shape
  exact IntegerNonnegative.ofNat with *

theorem IntegerPositive.ofNat_add_one (n : Nat)
  shows IntegerPositive(integerOfNat(n + 1))
proof
  witness n
  constructor
  . typecheck
  . rfl

theorem IntegerPositive.iff_sub_one (z : Integer)
  shows IntegerPositive(z) ↔ IntegerNonnegative(z - 1)
proof
  constructor
  . intro positive
    obtain ⟨n, nMember, shape⟩ := positive
    have nNat := nat.omega.backward with nMember
    have split := integerOfNat.add at n, 1
    have one : integerOfNat(1) = 1
      unfold integerOne
      rfl
    rw [shape, split, one]
    have cancel : integerOfNat(n) + 1 - 1 = integerOfNat(n) by ring
    rw cancel
    exact IntegerNonnegative.ofNat with *
  . intro nonnegative
    obtain ⟨n, nMember, shape⟩ := nonnegative
    have nNat := nat.omega.backward with nMember
    have split := integerOfNat.add at n, 1
    have one : integerOfNat(1) = 1
      unfold integerOne
      rfl
    have restore : z = (z - 1) + 1 by ring
    rw [restore, shape, ← one, ← split]
    exact IntegerPositive.ofNat_add_one with *

theorem IntegerPositive.mul (x y : Integer)
  requires first : IntegerPositive(x)
  requires second : IntegerPositive(y)
  shows IntegerPositive(x * y)
proof
  obtain ⟨n, nMember, xShape⟩ := first
  obtain ⟨m, mMember, yShape⟩ := second
  have nNat := nat.omega.backward with nMember
  have mNat := nat.omega.backward with mMember
  have product := integerMulValue.ofNat at n + 1, m + 1
  have expand : (n + 1) * (m + 1) = (n * m + n + m) + 1 by ring
  rw [xShape, yShape, product, expand]
  exact IntegerPositive.ofNat_add_one with *

theorem IntegerPositive.add (x y : Integer)
  requires first : IntegerPositive(x)
  requires second : IntegerPositive(y)
  shows IntegerPositive(x + y)
proof
  obtain ⟨n, nMember, xShape⟩ := first
  obtain ⟨m, mMember, yShape⟩ := second
  have nNat := nat.omega.backward with nMember
  have mNat := nat.omega.backward with mMember
  have sum := integerOfNat.add at n + 1, m + 1
  have expand : (n + 1) + (m + 1) = (n + m + 1) + 1 by ring
  rw [xShape, yShape, ← sum, expand]
  exact IntegerPositive.ofNat_add_one with *

theorem IntegerPositive.not_zero
  shows ¬IntegerPositive(integerZero)
proof
  intro positive
  obtain ⟨n, nMember, shape⟩ := positive
  have nNat := nat.omega.backward with nMember
  rw ← integerOfNat.zero at shape
  have same := integerOfNat.injective with shape
  have impossible : 0 < 0 by linarith
  exact Less.irreflexive with impossible

theorem integerLe.reflexive (x : Integer)
  shows x ≤ x
proof
  unfold integerLe
  have zero : x - x = 0 by ring
  rw zero
  exact IntegerNonnegative.zero

theorem integerLe.of_eq (x y : Integer)
  requires same : x = y
  shows x ≤ y
proof
  rw same
  exact integerLe.reflexive with *

theorem integerLe.transitive (x y z : Integer)
  requires first : x ≤ y
  requires second : y ≤ z
  shows x ≤ z
proof
  unfold integerLe at first
  unfold integerLe at second
  have sum : z - x = (z - y) + (y - x) by ring
  unfold integerLe
  rw sum
  exact IntegerNonnegative.add with second, first

theorem integerLe.antisymmetric (x y : Integer)
  requires first : x ≤ y
  requires second : y ≤ x
  shows x = y
proof
  unfold integerLe at first
  unfold integerLe at second
  have flip : x - y = -(y - x) by ring
  rw flip at second
  have zero := IntegerNonnegative.eq_zero with first, second
  have restore : x = y - (y - x) by ring
  rw [restore, zero]
  ring

theorem integerLe.total (x y : Integer)
  shows x ≤ y ∨ y ≤ x
proof
  have split := IntegerNonnegative.cases at y - x with *
  cases split with forward | backward
  . left
    exact forward
  . right
    have flip : x - y = -(y - x) by ring
    unfold integerLe
    rw flip
    exact backward

theorem integerLe.zero_iff (x : Integer)
  shows 0 ≤ x ↔ IntegerNonnegative(x)
proof
  have shape : x - 0 = x by ring
  constructor
  . intro below
    unfold integerLe at below
    rw shape at below
    exact below
  . intro nonnegative
    unfold integerLe
    rw shape
    exact nonnegative

theorem integerLe.sub_nonneg_iff (x y : Integer)
  shows x ≤ y ↔ 0 ≤ y - x
proof
  have difference := integerLe.zero_iff at y - x with *
  constructor
  . intro below
    unfold integerLe at below
    exact difference.backward with below
  . intro below
    have nonnegative := difference.forward with below
    unfold integerLe
    exact nonnegative

theorem integerLe.ofNat_nonneg (n : Nat)
  shows 0 ≤ integerOfNat(n)
proof
  apply integerLe.zero_iff.backward
  exact IntegerNonnegative.ofNat with *

theorem integerLe.negative_nonpos (n : Nat)
  shows integerNegativeOfNat(n) ≤ 0
proof
  unfold integerLe
  have flip : 0 - integerNegativeOfNat(n) = -(integerNegativeOfNat(n)) by ring
  rw [flip, integerNegativeOfNat.neg]
  exact IntegerNonnegative.ofNat with *

theorem integerLe.zero_one
  shows integerZero ≤ integerOne
proof
  unfold integerLe
  have shape : integerOne - integerZero = integerOne by ring
  rw shape
  exact IntegerNonnegative.one

theorem integerLe.add_right (x y z : Integer)
  requires below : x ≤ y
  shows x + z ≤ y + z
proof
  have shape : (y + z) - (x + z) = y - x by ring
  unfold integerLe
  rw shape
  exact below

theorem integerLe.add_left (x y z : Integer)
  requires below : x ≤ y
  shows z + x ≤ z + y
proof
  have shape : (z + y) - (z + x) = y - x by ring
  unfold integerLe
  rw shape
  exact below

theorem integerLe.add (a b c d : Integer)
  requires first : a ≤ b
  requires second : c ≤ d
  shows a + c ≤ b + d
proof
  have left := integerLe.add_right at a, b, c with first
  have right := integerLe.add_left at c, d, b with second
  exact integerLe.transitive with left, right

theorem integerLe.add_right_cancel (x y z : Integer)
  requires below : x + z ≤ y + z
  shows x ≤ y
proof
  have shape : (y + z) - (x + z) = y - x by ring
  unfold integerLe at below
  rw shape at below
  exact below

theorem integerLe.add_left_cancel (x y z : Integer)
  requires below : z + x ≤ z + y
  shows x ≤ y
proof
  have shape : (z + y) - (z + x) = y - x by ring
  unfold integerLe at below
  rw shape at below
  exact below

theorem integerLe.neg (x y : Integer)
  shows x ≤ y ↔ -y ≤ -x
proof
  have shape : (-x) - (-y) = y - x by ring
  constructor
  . intro below
    unfold integerLe
    rw shape
    exact below
  . intro below
    unfold integerLe at below
    rw shape at below
    exact below

theorem integerLe.neg_nonneg_iff (x : Integer)
  shows 0 ≤ -x ↔ x ≤ 0
proof
  have shape : (-x) - 0 = 0 - x by ring
  constructor
  . intro below
    unfold integerLe at below
    rw shape at below
    exact below
  . intro below
    unfold integerLe
    rw shape
    exact below

theorem integerLe.sub_right (x y z : Integer)
  requires below : x ≤ y
  shows x - z ≤ y - z
proof
  have shape : (y - z) - (x - z) = y - x by ring
  unfold integerLe
  rw shape
  exact below

theorem integerLe.sub_left (x y z : Integer)
  requires below : x ≤ y
  shows z - y ≤ z - x
proof
  have shape : (z - x) - (z - y) = y - x by ring
  unfold integerLe
  rw shape
  exact below

theorem integerLe.exists_natural (x y : Integer)
  requires below : x ≤ y
  shows ∃ n, Nat(n) ∧ y = x + integerOfNat(n)
proof
  unfold integerLe at below
  obtain ⟨n, nNat, shape⟩ := IntegerNonnegative.exists_natural with below
  witness n
  have restore : y = x + (y - x) by ring
  rw [restore, shape]
  rfl

theorem integerLe.of_natural (x y : Integer, n : Nat)
  requires shape : y = x + integerOfNat(n)
  shows x ≤ y
proof
  unfold integerLe
  rw shape
  have cancel : x + integerOfNat(n) - x = integerOfNat(n) by ring
  rw cancel
  exact IntegerNonnegative.ofNat with *

theorem integerLe.ofNat_iff (a b : Nat)
  shows integerOfNat(a) ≤ integerOfNat(b) ↔ a ≤ b
proof
  constructor
  . intro below
    obtain ⟨n, nNat, shape⟩ := integerLe.exists_natural with below
    have sum := integerOfNat.add at a, n
    rw ← sum at shape
    have same := integerOfNat.injective with shape
    witness n
    symm
    exact same
  . intro below
    obtain ⟨n, nNat, equation⟩ := below
    have sum := integerOfNat.add at a, n
    apply integerLe.of_natural at integerOfNat(a), integerOfNat(b), n
    rw [← sum, equation]
    rfl

theorem integerLe.cases_sign (x : Integer)
  shows 0 ≤ x ∨ x ≤ 0
proof
  have split := IntegerNonnegative.cases at x with *
  cases split with nonnegative | negative
  . left
    exact integerLe.zero_iff.backward with nonnegative
  . right
    have lifted := integerLe.zero_iff.backward with negative
    exact integerLe.neg_nonneg_iff.forward with lifted

theorem integerLe.exists_negative (x : Integer)
  requires nonpositive : x ≤ 0
  shows ∃ n, Nat(n) ∧ x = integerNegativeOfNat(n)
proof
  have negated := integerLe.neg_nonneg_iff.backward with nonpositive
  have nonnegative := integerLe.zero_iff.forward with negated
  obtain ⟨n, nNat, shape⟩ :=
    IntegerNonnegative.exists_natural with nonnegative
  witness n
  have restore : x = -(-x) by ring
  rw [restore, shape]
  exact integerOfNat.neg with *

theorem integerLess.iff_add_one_le (x y : Integer)
  shows x < y ↔ x + 1 ≤ y
proof
  constructor
  . intro below
    unfold integerLess at below
    exact below
  . intro below
    unfold integerLess
    exact below

theorem integerLess.zero_iff_positive (x : Integer)
  shows 0 < x ↔ IntegerPositive(x)
proof
  have shape : x - (integerZero + 1) = x - 1 by ring
  have positive := IntegerPositive.iff_sub_one at x with *
  constructor
  . intro below
    unfold integerLess at below
    unfold integerLe at below
    rw shape at below
    exact positive.backward with below
  . intro isPositive
    have nonnegative := positive.forward with isPositive
    unfold integerLess
    unfold integerLe
    rw shape
    exact nonnegative

theorem integerLess.sub_positive_iff (x y : Integer)
  shows x < y ↔ 0 < y - x
proof
  have shape : y - (x + 1) = (y - x) - (integerZero + 1) by ring
  constructor
  . intro below
    unfold integerLess at below
    unfold integerLe at below
    rw shape at below
    unfold integerLess
    unfold integerLe
    exact below
  . intro below
    unfold integerLess at below
    unfold integerLe at below
    unfold integerLess
    unfold integerLe
    rw shape
    exact below

theorem integerLess.add_one (x : Integer)
  shows x < x + 1
proof
  unfold integerLess
  exact integerLe.reflexive with *

theorem integerLe.add_one (x : Integer)
  shows x ≤ x + 1
proof
  apply integerLe.of_natural at x, x + 1, 1
  unfold integerOne
  rfl

theorem integerLess.implies_le (x y : Integer)
  requires below : x < y
  shows x ≤ y
proof
  unfold integerLess at below
  have step := integerLe.add_one at x
  exact integerLe.transitive with step, below

theorem integerLess.irreflexive (x : Integer)
  shows ¬x < x
proof
  intro below
  unfold integerLess at below
  unfold integerLe at below
  have shape : x - (x + 1) = integerNegativeOfNat(1)
    have flipped := integerOfNat.neg at 1
    unfold integerOne
    rw ← flipped
    ring
  rw shape at below
  have zero := IntegerNonnegative.negative_iff.forward with below
  have impossible : 0 < 1 by linarith
  rw zero at impossible
  exact Less.irreflexive with impossible

theorem integerLess.ne (x y : Integer)
  requires below : x < y
  shows x ≠ y
proof
  intro same
  rw same at below
  exact integerLess.irreflexive with below

theorem integerLess.transitive_le (x y z : Integer)
  requires first : x < y
  requires second : y ≤ z
  shows x < z
proof
  unfold integerLess at first
  unfold integerLess
  exact integerLe.transitive with first, second

theorem integerLe.transitive_less (x y z : Integer)
  requires first : x ≤ y
  requires second : y < z
  shows x < z
proof
  unfold integerLess at second
  unfold integerLess
  have step := integerLe.add_right at x, y, integerOne with first
  exact integerLe.transitive with step, second

theorem integerLess.transitive (x y z : Integer)
  requires first : x < y
  requires second : y < z
  shows x < z
proof
  have weak := integerLess.implies_le with second
  exact integerLess.transitive_le with first, weak

theorem integerLess.of_le_ne (x y : Integer)
  requires below : x ≤ y
  requires distinct : x ≠ y
  shows x < y
proof
  obtain ⟨n, nNat, shape⟩ := integerLe.exists_natural with below
  have split := natural.zero_or_successor at n
  cases split with zero | successor
  . rw [zero, integerOfNat.zero] at shape
    have same : x = y
      rw shape
      ring
    exfalso
    exact distinct with same
  . obtain ⟨k, kNat, equation⟩ := successor
    have step : succ(k) = k + 1 by ring
    rw [equation, step] at shape
    have sum := integerOfNat.add at k, 1
    have one : integerOfNat(1) = 1
      unfold integerOne
      rfl
    rw [sum, one] at shape
    unfold integerLess
    apply integerLe.of_natural at x + 1, y, k
    rw shape
    ring

theorem integerLess.iff_le_ne (x y : Integer)
  shows x < y ↔ x ≤ y ∧ x ≠ y
proof
  constructor
  . intro below
    exact ⟨integerLess.implies_le with below, integerLess.ne with below⟩
  . intro both
    exact integerLess.of_le_ne with both.left, both.right

theorem integerLe.cases (x y : Integer)
  requires below : x ≤ y
  shows x < y ∨ x = y
proof
  have split : x = y ∨ x ≠ y by tauto
  cases split with same | distinct
  . right
    exact same
  . left
    exact integerLess.of_le_ne with below, distinct

theorem integerLe.not_less (x y : Integer)
  requires below : x ≤ y
  shows ¬y < x
proof
  intro above
  have cycle := integerLess.transitive_le with above, below
  exact integerLess.irreflexive with cycle

theorem integerLess.not_le (x y : Integer)
  requires below : x < y
  shows ¬y ≤ x
proof
  intro above
  have cycle := integerLess.transitive_le with below, above
  exact integerLess.irreflexive with cycle

theorem integerLess.asymmetric (x y : Integer)
  requires below : x < y
  shows ¬y < x
proof
  have weak := integerLess.implies_le with below
  exact integerLe.not_less with weak

theorem integerLe.of_not_less (x y : Integer)
  requires notBelow : ¬x < y
  shows y ≤ x
proof
  have total := integerLe.total at x, y
  cases total with below | above
  . have split := integerLe.cases with below
    cases split with strict | same
    . exfalso
      exact notBelow with strict
    . rw same
      exact integerLe.reflexive with *
  . exact above

theorem integerLess.of_not_le (x y : Integer)
  requires notBelow : ¬x ≤ y
  shows y < x
proof
  have total := integerLe.total at x, y
  cases total with below | above
  . exfalso
    exact notBelow with below
  . have distinct : y ≠ x
      intro same
      rw same at notBelow
      exact notBelow with (integerLe.reflexive at x)
    exact integerLess.of_le_ne with above, distinct

theorem integerLess.trichotomy (x y : Integer)
  shows x < y ∨ x = y ∨ y < x
proof
  have total := integerLe.total at x, y
  cases total with below | above
  . have split := integerLe.cases with below
    cases split with strict | same
    . left
      exact strict
    . right
      left
      exact same
  . have split := integerLe.cases with above
    cases split with strict | same
    . right
      right
      exact strict
    . right
      left
      symm
      exact same

theorem integerLess.add_right (x y z : Integer)
  requires below : x < y
  shows x + z < y + z
proof
  unfold integerLess at below
  unfold integerLess
  have shape : x + z + 1 = (x + 1) + z by ring
  rw shape
  exact integerLe.add_right with below

theorem integerLess.add_left (x y z : Integer)
  requires below : x < y
  shows z + x < z + y
proof
  have shifted := integerLess.add_right at x, y, z with below
  have left : x + z = z + x by ring
  have right : y + z = z + y by ring
  rw [left, right] at shifted
  exact shifted

theorem integerLess.add_le (a b c d : Integer)
  requires first : a < b
  requires second : c ≤ d
  shows a + c < b + d
proof
  have left := integerLess.add_right at a, b, c with first
  have right := integerLe.add_left at c, d, b with second
  exact integerLess.transitive_le with left, right

theorem integerLe.add_less (a b c d : Integer)
  requires first : a ≤ b
  requires second : c < d
  shows a + c < b + d
proof
  have left := integerLe.add_right at a, b, c with first
  have right := integerLess.add_left at c, d, b with second
  exact integerLe.transitive_less with left, right

theorem integerLess.add (a b c d : Integer)
  requires first : a < b
  requires second : c < d
  shows a + c < b + d
proof
  have weak := integerLess.implies_le with second
  exact integerLess.add_le with first, weak

theorem integerLess.add_right_cancel (x y z : Integer)
  requires below : x + z < y + z
  shows x < y
proof
  have shifted := integerLess.add_right at x + z, y + z, -z with below
  have left : x + z + (-z) = x by ring
  have right : y + z + (-z) = y by ring
  rw [left, right] at shifted
  exact shifted

theorem integerLess.neg (x y : Integer)
  shows x < y ↔ -y < -x
proof
  have shape : (-x) - (-y + 1) = y - (x + 1) by ring
  constructor
  . intro below
    unfold integerLess at below
    unfold integerLe at below
    unfold integerLess
    unfold integerLe
    rw shape
    exact below
  . intro below
    unfold integerLess at below
    unfold integerLe at below
    rw shape at below
    unfold integerLess
    unfold integerLe
    exact below

theorem integerLess.zero_one
  shows integerZero < integerOne
proof
  unfold integerLess
  have shape : integerZero + 1 = integerOne by ring
  rw shape
  exact integerLe.reflexive with *

theorem integerLess.ofNat_iff (a b : Nat)
  shows integerOfNat(a) < integerOfNat(b) ↔ a < b
proof
  have sum := integerOfNat.add at a, 1
  have one : integerOfNat(1) = 1
    unfold integerOne
    rfl
  have gap := Less.gap at a, b
  have bridge := integerLe.ofNat_iff at a + 1, b
  constructor
  . intro below
    unfold integerLess at below
    rw [← one, ← sum] at below
    have weak := bridge.forward with below
    exact gap.backward with weak
  . intro below
    have weak := gap.forward with below
    have lifted := bridge.backward with weak
    unfold integerLess
    rw [← one, ← sum]
    exact lifted

theorem integerLess.one_le_of_positive (x : Integer)
  requires positive : 0 < x
  shows 1 ≤ x
proof
  unfold integerLess at positive
  have shape : integerZero + 1 = integerOne by ring
  rw shape at positive
  exact positive

theorem integerLess.not_between (x y : Integer)
  requires first : x < y
  requires second : y < x + 1
  shows ⊥
proof
  unfold integerLess at first
  unfold integerLess at second
  have cancelled := integerLe.add_right_cancel at y, x, integerOne with second
  have cycle := integerLe.transitive with first, cancelled
  exact integerLess.irreflexive at x with cycle