proposition: Lemma of_iff d d' : of_decimal d = of_decimal d' <-> dnorm d = dnorm d'.
proof: Proof. split. - apply of_inj. - intros E. rewrite <- of_decimal_dnorm, E. apply of_decimal_dnorm. Qed.
imports: Decimal DecimalFacts DecimalPos DecimalN DecimalZ QArith