proposition: Lemma of_decimal_dnorm d : of_decimal (dnorm d) = of_decimal d.
proof: Proof. now apply to_decimal_inj; rewrite !to_of; [|rewrite dnorm_involutive]. Qed.
imports: Decimal DecimalFacts DecimalPos DecimalN DecimalZ QArith