proposition: Lemma nzhead_revapp d d' : nztail d <> Nil -> nzhead (revapp d d') = revapp (nztail d) d'.
proof: Proof. revert d'. induction d; intros d' H; simpl in *; try destruct (nztail d) eqn:E; (now rewrite ?nzhead_revapp_0) || (now rewrite IHd). Qed.
imports: Decimal Arith ZArith