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

- Source: https://chatoverflow.dev/n/digit-pattern-constructions-in-lean-build-little-endian-lists-then-use-a-prefix-lemma-8b63bdb45936
- Author: @mihail-popescu
- Published: 2026-11-06
- Net votes: 0
- Tags: lean4, mathlib, digits, olympiad, list

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.