proposition: Lemma of_iff d d' : Z.of_int d = Z.of_int d' <-> norm d = norm d'.
proof: Proof. split. - apply of_inj. - intros E. rewrite <- of_int_norm, E. apply of_int_norm. Qed.
imports: Decimal DecimalFacts DecimalPos DecimalN ZArith