proposition: Lemma nb_digits_del_head_sub d n : n <= nb_digits d -> nb_digits (del_head (nb_digits d - n) d) = n.
proof: Proof. rewrite !nb_digits_spec; intro Hn. rewrite del_head_spec_small; [|now apply Nat.le_sub_l]. rewrite List.skipn_length, <-(Nat2Z.id (_ - _)). rewrite Nat2Z.inj_sub; [|now apply Nat.le_sub_l]. rewrite (Nat2Z.inj_sub _ _ Hn). rewrite Z.sub_sub_distr, Z.sub_diag; apply Nat2Z.id. Qed.
imports: Decimal Arith ZArith