proposition: Lemma of_lu_revapp d d' : of_lu (revapp d d') = of_lu (rev d) + of_lu d' * 10^usize d.
proof: Proof. revert d'. induction d; simpl; intro d'; [ now rewrite N.mul_1_r | .. ]; unfold rev; simpl revapp; rewrite 2 IHd; rewrite <- N.add_assoc; f_equal; simpl_of_lu; simpl of_lu; rewrite N.pow_succ_r'; ring. Qed.
imports: Decimal DecimalFacts PArith NArith