proposition: Lemma del_head_app n d d' : n <= nb_digits d -> del_head n (app d d') = app (del_head n d) d'.
proof: Proof. rewrite nb_digits_spec; intro Hn. apply to_list_inj. rewrite del_head_spec_small. 2:{ now rewrite app_spec, List.app_length, <- Nat.le_add_r. } rewrite !app_spec, (del_head_spec_small _ _ Hn). rewrite List.skipn_app. now rewrite (proj2 (Nat.sub_0_le _ _) Hn). Qed.
imports: Decimal Arith ZArith