proposition: Lemma nb_digits_unorm u : u <> Nil -> nb_digits (unorm u) <= nb_digits u.
proof: Proof. intro Hu; case (uint_eq_dec (nzhead u) Nil). { unfold unorm; intros ->; simpl. now revert Hu; case u; [|intros u' _; apply le_n_S, Nat.le_0_l..]. } intro H; rewrite (unorm_nzhead _ H); apply nb_digits_nzhead. Qed.
imports: Decimal Arith ZArith