proposition: Lemma of_uint_acc_rev d acc : Npos (Pos.of_uint_acc d acc) = of_lu (rev d) + (Npos acc) * 10^usize d.
proof: Proof. revert acc. induction d; intros; simpl usize; [ simpl; now rewrite Pos.mul_1_r | .. ]; rewrite N.pow_succ_r'; unfold rev; simpl revapp; try rewrite of_lu_revapp; simpl of_lu; rewrite of_uint_acc_eqn by easy; simpl tl; simpl hd; rewrite IHd, Nadd_simpl; ring. Qed.
imports: Decimal DecimalFacts PArith NArith