proposition: Lemma rdigitnSMl b m n : 0 < b -> rdigitn b n.+1 m = (m %% b) * b ^ n + rdigitn b n (m %/ b).
proof: Proof. move=> b_gt0. rewrite !rdigitnE big_ord_recr addnC /= subnn digitn0; congr (_ + _). apply: eq_bigr => i _. have n_gt0 : 0 < n by apply: leq_ltn_trans (_ : i < n)%N. by rewrite -[X in X - i](prednK n_gt0) subSn ?digitnS // -ltnS prednK. Qed.
imports: mathcomp(all_ssreflect) mathcomp(all_algebra)