proposition: Lemma ltn_rdigitn b n m : 0 < b -> rdigitn b n m < b ^ n.
proof: Proof. move=> b_gt0. elim: n m => [n |n IH m]; first by rewrite rdigit0n. rewrite rdigitnSMl // -addnS addnC. 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_mod. Qed.
imports: mathcomp(all_ssreflect) mathcomp(all_algebra)