English
The result of comparing m and n via cmp corresponds to the usual order on integers: if m ≤ n, then etc.
Русский
Результат сравнения m и n через cmp соответствует обычному порядку на целых: если m ≤ n, и т.д.
LaTeX
$$$$\forall m,n \in ZNum,\ (Ordering.casesOn (cmp\, m\, n) (m : \mathbb{Z}) < n) (m = n) ((n : \mathbb{Z}) < m) : Prop.$$$$
Lean4
theorem cmp_to_int : ∀ m n, (Ordering.casesOn (cmp m n) ((m : ℤ) < n) (m = n) ((n : ℤ) < m) : Prop)
| 0, 0 => rfl
| pos a, pos b => by
have := PosNum.cmp_to_nat a b; revert this; dsimp [cmp]
cases PosNum.cmp a b <;> [simp; exact congr_arg pos; simp]
| neg a, neg b => by
have := PosNum.cmp_to_nat b a; revert this; dsimp [cmp]
cases PosNum.cmp b a <;> [simp; simp +contextual; simp]
| pos _, 0 => PosNum.cast_pos _
| pos _, neg _ => lt_trans (neg_lt_zero.2 <| PosNum.cast_pos _) (PosNum.cast_pos _)
| 0, neg _ => neg_lt_zero.2 <| PosNum.cast_pos _
| neg _, 0 => neg_lt_zero.2 <| PosNum.cast_pos _
| neg _, pos _ => lt_trans (neg_lt_zero.2 <| PosNum.cast_pos _) (PosNum.cast_pos _)
| 0, pos _ => PosNum.cast_pos _
