proposition: Lemma nztail_involutive d : nztail (nztail d) = nztail d.
proof: Proof. rewrite <-(rev_rev (nztail _)), <-(rev_rev (nztail d)), <-(rev_rev d). now rewrite !rev_nztail_rev, nzhead_involutive. Qed.
imports: Decimal Arith ZArith