proposition: Lemma iter_D0_unorm d : d <> Nil -> Nat.iter (nb_digits d - nb_digits (unorm d)) D0 (unorm d) = d.
proof: Proof. case (uint_eq_dec (nzhead d) Nil); intro Hn. { unfold unorm; rewrite Hn; simpl; intro H. revert H Hn; induction d; [now simpl|intros _|now intros _..]. case (uint_eq_dec d Nil); simpl; intros H Hn; [now rewrite H|]. rewrite Nat.sub_0_r, <- (Nat.sub_add 1 (nb_digits d)), Nat.add_comm. { now simpl; rewrite IHd. } revert H; case d; [now simpl|intros u _; apply le_n_S, Nat.le_0_l..]. } intros _; rewrite (unorm_nzhead _ Hn); apply iter_D0_nzhead. Qed.
imports: Decimal Arith ZArith