proposition: Lemma rdigitnK b n m : m < b ^ n -> rdigitn b n (rdigitn b n m) = m.
proof: Proof. have [|b_gt0] := leqP b 0. by case: b; case: n; case: m => //= [n|n m]; rewrite exp0n. move=> mLbn. rewrite {1}rdigitnE [RHS](digitnE mLbn). apply: eq_bigr => i _; congr (_ * _). rewrite rdigitnE. pose f1 := [ffun i : 'I_n => (Ordinal (@ltn_pdigit b m (n.-1 - i) b_gt0)) ]. have G : \sum_(i < n) digitn b m (n.-1 - i) * b ^ i = \sum_(i < n) (f1 i * b ^ i). by apply: eq_bigr => j _; rewrite ffunE. have n_gt0 : 0 < n by case: i; case: (n). have FF : n.-1 - i < n. apply: leq_ltn_trans (leq_subr _ _) _. by rewrite prednK. have <- := digitn_uniq (Ordinal FF) _ G. rewrite ffunE /= subnA //; first by rewrite subnn. by rewrite -ltnS prednK. move: n.-1 => u; elim: {i f1 G mLbn n_gt0 FF}n => [|n IH]. by rewrite big_ord0 expn0. rewrite big_ord_recr /= -addSn. have -> : b ^ n.+1 = b ^ n + b.-1 * b ^ n. by rewrite expnS -[X in X * _ = _](prednK b_gt0) mulSn. rewrite leq_add // leq_mul2r expn_eq0 eqn0Ngt b_gt0 /= -ltnS prednK //. by rewrite ltn_pdigit. Qed.
imports: mathcomp(all_ssreflect) mathcomp(all_algebra)