proposition: Lemma digitnE b n m : n < b ^ m -> n = \sum_(i < m) digitn b n i * b ^ i.
proof: Proof. elim: m n => [[]//=|m IH n nLb]; first by rewrite big_ord0. rewrite {1}(divn_eq n b) [n %/ b]IH; last first. rewrite (divn_eq n b) in nLb. have := leq_ltn_trans (leq_addr _ _) nLb. by rewrite expnS mulnC ltn_mul2l => /andP[]. rewrite big_ord_recl addnC digitn0 muln1; congr (_ + _). rewrite (big_morph _ (fun x y => mulnDl x y b) (mul0n b)). apply: eq_bigr => /= i _. by rewrite digitnS expnS mulnAC mulnA. Qed.
imports: mathcomp(all_ssreflect) mathcomp(all_algebra)