proposition: Lemma to_ldec_tenfold p : to_lu (10 * Npos p) = D0 (to_lu (Npos p)).
proof: Proof. induction p using Pos.peano_rect. - trivial. - change (N.pos (Pos.succ p)) with (N.succ (N.pos p)). rewrite N.mul_succ_r. change 10 with (Nat.iter 10%nat N.succ 0) at 2. rewrite ?nat_iter_S, nat_iter_0. rewrite !N.add_succ_r, N.add_0_r, !to_lu_succ, IHp. destruct (to_lu (N.pos p)); simpl; auto. Qed.
imports: Decimal DecimalFacts PArith NArith