English
If x < 2^n and y < 2^m, then the concatenation of y in higher bits with x in lower bits is less than 2^{n+m}.
Русский
Если x < 2^n и y < 2^m, то конкатенация y в старших разрядах и x в младших меньше чем 2^{n+m}.
LaTeX
$$$ (y \cdot 2^{n} + x) < 2^{n+m} \quad\text{при } x < 2^{n}, \; y < 2^{m} $$$
Lean4
/-- Note that the LHS is the expression used within `Std.BitVec.append`, hence the name. -/
theorem append_lt {x y n m} (hx : x < 2 ^ n) (hy : y < 2 ^ m) : y <<< n ||| x < 2 ^ (n + m) :=
by
apply bitwise_lt_two_pow
· rw [add_comm]; apply shiftLeft_lt hy
· apply lt_of_lt_of_le hx <| Nat.pow_le_pow_right (le_succ _) (le_add_right _ _)
