proposition: Lemma nzhead_app_nil_l d d' : nzhead (app d d') = Nil -> nzhead d = Nil.
proof: Proof. intro H; apply to_list_inj; generalize (f_equal to_list H); clear H. rewrite !nzhead_spec, app_spec. induction (to_list d) as [|h t IHl]; [now simpl|]. now rewrite <-List.app_comm_cons; case h. Qed.
imports: Decimal Arith ZArith