proposition: Lemma rdigitnE b n m : rdigitn b n m = \sum_(i < n) digitn b m (n.-1 - i) * b ^ i.
proof: Proof. have <- := (big_mkord xpredT (fun i : nat => digitn b m (n.-1 - i) * b ^ i)). by rewrite unlock. Qed.
imports: mathcomp(all_ssreflect) mathcomp(all_algebra)