proposition: Lemma of_uint_iter_D0 d n : Z.of_uint (app d (Nat.iter n D0 Nil)) = Nat.iter n (Z.mul 10) (Z.of_uint d).
proof: Proof. rewrite <-(rev_rev (app _ _)), <-(of_list_to_list (rev (app _ _))). rewrite rev_spec, app_spec, List.rev_app_distr. rewrite <-!rev_spec, <-app_spec, of_list_to_list. unfold Z.of_uint; rewrite Unsigned.of_lu_rev. unfold app; rewrite Unsigned.of_lu_revapp, !rev_rev. rewrite <-!Unsigned.of_lu_rev, !rev_rev. assert (H' : Pos.of_uint (Nat.iter n D0 Nil) = 0%N). { now induction n; [|rewrite Unsigned.nat_iter_S]. } rewrite H', N.add_0_l; clear H'. induction n; [now simpl; rewrite N.mul_1_r|]. rewrite !Unsigned.nat_iter_S, <-IHn. simpl Unsigned.usize; rewrite N.pow_succ_r'. rewrite !N2Z.inj_mul; simpl Z.of_N; ring. Qed.
imports: Decimal DecimalFacts DecimalPos DecimalN ZArith