Binary sizes of products, powers, and factorials

These pure facts are moved unchanged from the binary arithmetic facade. They retain their qualified names without depending on a machine calculus.

theorem Nat.size_mul_le (m n : ℕ) : (m * n).size ≤ m.size + n.size

The binary length of a product is at most the binary lengths of the factors together.

theorem Nat.size_pow_le (m k : ℕ) : (m ^ k).size ≤ k * m.size + 1

The binary length of a power is at most the exponent times the binary length of the base, plus one for the zeroth power.

theorem Nat.size_factorial_le (n : ℕ) : n.factorial.size ≤ n * n.size + 1

The binary length of n! is at most n * n.size + 1.