proposition: Lemma to_of_lu d : to_lu (of_lu d) = lnorm d.
proof: Proof. induction d; [reflexivity|..]; simpl_of_lu; rewrite Nadd_alt; simpl_to_nat; rewrite ?nat_iter_S, nat_iter_0, ?to_lu_succ, to_of_lu_tenfold by assumption; unfold lnorm; simpl; destruct nztail; auto. Qed.
imports: Decimal DecimalFacts PArith NArith