proposition: Lemma to_of (d:uint) : N.to_uint (Pos.of_uint d) = unorm d.
proof: Proof. rewrite of_uint_alt. unfold N.to_uint, Pos.to_uint. destruct (of_lu (rev d)) eqn:H. - rewrite of_lu_0 in H. rewrite <- rev_lnorm_rev. unfold lnorm. now rewrite H. - change (Pos.to_little_uint p) with (to_lu (N.pos p)). rewrite <- H. rewrite to_of_lu. apply rev_lnorm_rev. Qed.
imports: Decimal DecimalFacts PArith NArith