no goals
x : ℕ
b : Bool
⊢ decide (addLsb x b % 2 = 1) = b
cases b <;>
    simp only [Bool.decide_iff, Nat.add_mul_mod_self_left, addLsb, ← two_mul, add_comm,
      Bool.decide_False, Nat.mul_mod_right, zero_add, cond, zero_ne_one]