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