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