rw [prepend_two, prepend_two]
n : ℕ
hn : 0 < n
⊢ prepend_two n / 10 = prepend_two (n / 10)
n : ℕ
hn : 0 < n
⊢ (2 * 10 ^ (Nat.digits 10 n).length + n) / 10 = 2 * 10 ^ (Nat.digits 10 (n / 10)).length + n / 10