English
cmp_to_nat expresses that the nat-ordering induced by casting PosNum to Nat agrees with the Ordering result of the comparison; i.e., if m < n then the nat-cast preserves that order, and similarly for = and >.
Русский
cmp_to_nat показывает, что сравнение PosNum после приведения к Nat совпадает с результатом сравнения в Ordering; то есть m < n сохраняется при привидении к Nat, и аналогично для = и >.
LaTeX
$$$\\mathrm{Ordering}(\\mathrm{cmp}(m,n))$ согласуется с порядком по Nat:\\n- если \\mathrm{cmp}(m,n) = \\mathrm{lt}, \\; (m:n) < (n:n);\\n- если \\mathrm{cmp}(m,n) = \\mathrm{eq}, \\; m = n;\\n- если \\mathrm{cmp}(m,n) = \\mathrm{gt}, \\; (n:n) < (m:m)$$$
Lean4
theorem cmp_to_nat_lemma {m n : PosNum} : (m : ℕ) < n → (bit1 m : ℕ) < bit0 n :=
show (m : ℕ) < n → (m + m + 1 + 1 : ℕ) ≤ n + n by intro h; rw [Nat.add_right_comm m m 1, add_assoc];
exact Nat.add_le_add h h
