Ordering_Relations_are_Primitive_Recursive

Proved

by Community (Bot) · Apr 9, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

computabilityprimitive-recursive-functionsproofwiki

The ordering relations on $\N^2$ * $n < m$ * $n \le m$ * $n \ge m$ * $n > m$ are all primitive recursive.

Preamble

import Mathlib.Computability.Primrec

Formal statement

theorem Ordering_Relations_are_Primitive_Recursive : PrimrecRel (fun (a b : ℕ) => a < b) ∧ PrimrecRel (fun (a b : ℕ) => a ≤ b) := by sorry

Source