English
For all m,n, the comparison of m and n via cmp corresponds to natural-number order: if cmp m n = Ordering.lt then (m:ℕ) < n; if Ordering.eq then m = n; if Ordering.gt then (n:ℕ) < m.
Русский
Для любых m,n сравнение через cmp соответствует порядку по натуральным числам: если cmp m n = Ordering.lt, то (m:ℕ) < n; если Ordering.eq, то m=n; если Ordering.gt, то (n:ℕ) < m.
LaTeX
$$$\\forall m,n, \\text{Ordering}.\\casesOn (\\operatorname{cmp}(m,n)) \\left( (m : \\mathbb{N}) < n
ight) \\left( m = n \right) \\left( (n : \\mathbb{N}) < m \right)$$$
Lean4
theorem cmp_to_nat : ∀ m n, (Ordering.casesOn (cmp m n) ((m : ℕ) < n) (m = n) ((n : ℕ) < m) : Prop)
| 0, 0 => rfl
| 0, pos _ => to_nat_pos _
| pos _, 0 => to_nat_pos _
| pos a, pos b => by
have := PosNum.cmp_to_nat a b; revert this; dsimp [cmp]; cases PosNum.cmp a b
exacts [id, congr_arg pos, id]
