`conv {to_rhs, ...}` behaves poorly with `nat.modeq`.

Mario helped me write a proof:

lemma foo (n k : ℕ) : k ≡ ((k / 2^n) + (k % 2^n)) [MOD 2^n - 1] :=
-- See https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/help.20finding.20a.20lemma/near/177698446
begin
  conv {to_rhs, rw [← nat.mod_add_div k (2^n), add_comm]},
  refine nat.modeq.modeq_add _ (by refl),
  conv {to_rhs, skip, rw ← one_mul (k/2^n)},
  refine nat.modeq.modeq_mul _ (by refl),
  symmetry,
  rw [nat.modeq.modeq_iff_dvd, int.coe_nat_sub],
  exact nat.pow_pos dec_trivial _
end

in which both instances of to_rhs are a bit strange. The first one actually looks at the left-hand-side, while the second one requires a skip before actually reaching the right-hand-side.

Start by reproducing the supplied proof and tracing both conv {to_rhs, ...} uses alongside nat.modeq. Compare the traversal behavior in the first case with the second case that needs skip, then verify that the resulting behavior is consistent for both examples.