English
For all integers m and natural numbers n,k, shifting m left by (n+k) equals shifting m left by n and then by k.
Русский
Для любых m ∈ ℤ и чисел n,k ∈ ℕ: m <<< (n+k) = (m <<< n) <<< k.
LaTeX
$$$$ \forall m\in\mathbb{Z},\; \forall n,k\in\mathbb{N},\; m\ <<<\ (n+k) = (m\ <<<\ n)\ <<<\ k. $$$$
Lean4
/-- Compare with `Int.shiftRight_add`, which doesn't have the coercions `ℕ → ℤ`. -/
theorem shiftRight_add' : ∀ (m : ℤ) (n k : ℕ), m >>> (n + k : ℤ) = (m >>> (n : ℤ)) >>> (k : ℤ)
| (m : ℕ), n, k => by
rw [shiftRight_natCast, shiftRight_natCast, ← Int.natCast_add, shiftRight_natCast, Nat.shiftRight_add]
| -[m+1], n, k => by
rw [shiftRight_negSucc, shiftRight_negSucc, ← Int.natCast_add, shiftRight_negSucc, Nat.shiftRight_add]
