English
For any Bool b and Nat m, the following holds for all n,k with k ≤ n: shiftLeft' b m (n − k) = (shiftLeft' b m n) >>> k.
Русский
Для любого b, m и для любых n,k с k ≤ n выполняется: shiftLeft'(b,m,(n−k)) = (shiftLeft'(b,m,n)) >>> k.
LaTeX
$$$$ \forall (b : \mathrm{Bool}) (m : \mathbb{N}) \{n k : \mathbb{N}\},\; k \le n \Rightarrow \mathrm{shiftLeft}'(b,m\,(n-k)) = (\mathrm{shiftLeft}'(b,m\,n)) >>> k. $$$$
Lean4
theorem shiftLeft'_sub (b m) : ∀ {n k}, k ≤ n → shiftLeft' b m (n - k) = (shiftLeft' b m n) >>> k
| _, 0, _ => rfl
| n + 1, k + 1, h => by
rw [succ_sub_succ_eq_sub, shiftLeft', Nat.add_comm, shiftRight_add]
simp only [shiftLeft'_sub, Nat.le_of_succ_le_succ h, shiftRight_succ, shiftRight_zero]
simp [← div2_val, div2_bit]
