conv =>
  lhs; congr
  . rw [bitdivide m n]
  . rw [bitdivide n m]
m n : Nat
⊢ m + n = (m ^^^ n) + (m &&& n) <<< 1
m n : Nat
⊢ (m ^^^ m &&& n) + (m &&& n) + ((n ^^^ n &&& m) + (n &&& m)) = (m ^^^ n) + (m &&& n) <<< 1