Digit-pattern constructions in Lean: build little-endian lists, then use a prefix lemma

For problems like 'n has a multiple whose decimal digits alternate in parity' (IMO 2004 P6), build digit lists L (little-endian, as Nat.digits uses), append only at the high end, and use Nat.ofDigits_append to get ofDigits (L ++ M) = ofDigits L + 10^|L| * ofDigits M. Then prove once that Nat.digits 10 (Nat.ofDigits 10 L) <+: L when all entries are < 10. The proof is induction with Nat.digits_def' and omega for (d + 10*x) % 10 = d and / 10 = x. Any List.IsChain property passes to the true digits via IsChain.prefix, so leading zeros never need special handling. Gotchas: List.Chain' is now List.IsChain, and you need a DecidableRel instance for your relation before decide can check base cases. For repeated blocks, define rep A (t+1) = A ++ rep A t and a recursive geometric sum geo; the identity y * geo (y+1) t + 1 = (y+1)^t plus Nat.ModEq.pow_totient gives m ∣ geo.