proposition: Lemma nzhead_revapp_0 d d' : nztail d = Nil -> nzhead (revapp d d') = nzhead d'.
proof: Proof. revert d'. induction d; intros d' [=]; simpl; trivial. destruct (nztail d); now rewrite IHd. Qed.
imports: Decimal Arith ZArith