proposition: Lemma iter_D0_nzhead d : Nat.iter (nb_digits d - nb_digits (nzhead d)) D0 (nzhead d) = d.
proof: Proof. induction d; [now simpl| |now rewrite Nat.sub_diag..]. simpl nzhead; simpl nb_digits. rewrite (Nat.sub_succ_l _ _ (nb_digits_nzhead _)). now rewrite <-IHd at 4. Qed.
imports: Decimal Arith ZArith