proposition: Lemma nzhead_app_l d d' : nb_digits d' < nb_digits (nzhead (app d d')) -> nzhead (app d d') = app (nzhead d) d'.
proof: Proof. intro Hl; apply to_list_inj; revert Hl. rewrite !nb_digits_spec, app_spec, !nzhead_spec, app_spec. induction (to_list d) as [|h t IHl]. { now simpl; intro H; exfalso; revert H; apply Nat.le_ngt, length_lnzhead. } rewrite <-List.app_comm_cons. now case h; [simpl; intro Hl; apply IHl|..]. Qed.
imports: Decimal Arith ZArith