proposition: Lemma digitn_uniq b n k (f : {ffun 'I_k -> 'I_b}) i : n < b ^ k -> n = (\sum_(i < k) f i * b ^ i)%N -> f i = digitn b n i :> nat.
proof: Proof. elim: k n f i => [n f [] //|k IH n f i nLb]. have b_pos : 0 < b by case: (b) nLb => //; rewrite exp0n. rewrite big_ord_recl /= muln1 => nE. have f0E : f ord0 = n %% b :> nat. rewrite nE -modnDm -modn_summ big1 => [| j _]. by rewrite mod0n addn0 modn_mod modn_small. by rewrite /bump add1n expnS mulnCA modnMr. have /IH H : n %/ b = \sum_(i < k) [ffun i => f (lift ord0 i)] i * b ^ i. move/eqP: nE. rewrite f0E {1}(divn_eq n b) addnC eqn_add2l. under eq_bigr do rewrite /bump add1n expnS mulnCA. rewrite -big_distrr /= mulnC eqn_mul2l. rewrite eqn_leq leqNgt b_pos /= => /eqP->. by apply: eq_bigr => j _; rewrite !ffunE. case i => [] [Hi|j Hj] /=. by rewrite digitn0 -f0E; congr (f _); apply/val_eqP. rewrite digitnS. have <- := H (Ordinal (Hj : j < k)). by rewrite ffunE /=; congr (f _); apply/val_eqP. by rewrite ltn_divLR // mulnC -expnS. Qed.
imports: mathcomp(all_ssreflect) mathcomp(all_algebra)