English
For all m, n ∈ ℕ, size m ≤ n if and only if m < 2^n.
Русский
Для всех m, n ∈ ℕ выполняется size(m) ≤ size(n) ↔ m < 2^n.
LaTeX
$$$\operatorname{size}(m) \le n \;\Leftrightarrow \; m < 2^{n}$$$
Lean4
theorem size_le {m n : ℕ} : size m ≤ n ↔ m < 2 ^ n :=
⟨fun h => lt_of_lt_of_le (lt_size_self _) (Nat.pow_le_pow_right (by decide) h),
by
rw [← one_shiftLeft]
induction m using binaryRec generalizing n with
| zero => simp
| bit b m IH =>
intro h
by_cases e : bit b m = 0
· simp [e]
rw [size_bit e]
cases n with
| zero => exact e.elim (Nat.eq_zero_of_le_zero (le_of_lt_succ h))
| succ n =>
apply succ_le_succ (IH _)
apply Nat.lt_of_mul_lt_mul_left (a := 2)
simp only [shiftLeft_succ] at *
refine lt_of_le_of_lt ?_ h
cases b <;> dsimp [bit] <;> omega⟩
