proposition: Lemma rev_lnorm_rev d : rev (lnorm (rev d)) = unorm d.
proof: Proof. unfold unorm, lnorm. rewrite <- rev_nztail_rev. destruct nztail; simpl; trivial; destruct rev eqn:E; trivial; now apply rev_nil_inv in E. Qed.
imports: Decimal Arith ZArith