b : Bool
m n k : ℕ
h : k + 1 ≤ n + 1
⊢ shiftl' b m (n - k) = shiftr (bit b (shiftl' b m n)) (k + 1)
b : Bool
m n k : ℕ
h : k + 1 ≤ n + 1
⊢ shiftl' b m (n + 1 - (k + 1)) = shiftr (shiftl' b m (n + 1)) (k + 1)
simp [shiftl']
b : Bool
m n k : ℕ
h : k + 1 ≤ n + 1
⊢ shiftl' b m (n - k) = shiftr (shiftr (bit b (shiftl' b m n)) 1) k
b : Bool
m n k : ℕ
h : k + 1 ≤ n + 1
⊢ shiftl' b m (n - k) = shiftr (bit b (shiftl' b m n)) (k + 1)
rw [Nat.add_comm, shiftr_add]
b : Bool
m n k : ℕ
h : k + 1 ≤ n + 1
⊢ shiftl' b m (n - k) = shiftr (shiftl' b m n) k
b : Bool
m n k : ℕ
h : k + 1 ≤ n + 1
⊢ shiftl' b m (n - k) = shiftr (shiftr (bit b (shiftl' b m n)) 1) k
simp [shiftr, div2_bit]
no goals
b : Bool
m n k : ℕ
h : k + 1 ≤ n + 1
⊢ shiftl' b m (n - k) = shiftr (shiftl' b m n) k
simp [shiftl'_sub, (Nat.le_of_succ_le_succ h)]