conv =>
  lhs;
  dsimp [HOr.hOr, OrOp.or, Nat.lor]; unfold bitwise
  rw [if_neg Nat.one_ne_zero, Bool.false_or, if_pos rfl]
  zeta
  rw [decide_eq_false hn2_neq_1, Bool.false_or, decide_eq_true, if_pos rfl]
  change if n = 0 then 1 else ((n/2) ||| 0) + ((n/2) ||| 0) + 1
  rw [Nat.lor_zero, ←Nat.mul_two]
  rw [Nat.div_mul_cancel ((Nat.dvd_iff_mod_eq_zero 2 n).mpr hn)]
n : Nat
hn : n % 2 = 0
hn2_neq_1 : n % 2 ≠ 1
⊢ n ||| 1 = n + 1
n : Nat
hn : n % 2 = 0
hn2_neq_1 : n % 2 ≠ 1
⊢ (if n = 0 then 1 else n + 1) = n + 1