proposition: Lemma of_iff d d' : N.of_uint d = N.of_uint d' <-> unorm d = unorm d'.
proof: Proof. split. - apply of_inj. - intros E. rewrite <- of_uint_norm, E. apply of_uint_norm. Qed.
imports: Decimal DecimalFacts DecimalPos PArith NArith