proposition: Lemma of_inj d d' : of_decimal d = of_decimal d' -> dnorm d = dnorm d'.
proof: Proof. intro H. apply (@f_equal _ _ (fun x => match x with Some x => x | _ => d end) (Some (dnorm d)) (Some (dnorm d'))). now rewrite <- !to_of, H. Qed.
imports: Decimal DecimalFacts DecimalPos DecimalN DecimalZ QArith