proposition: Lemma of_iff d d' : of_hexadecimal d = of_hexadecimal d' <-> dnorm d = dnorm d'.
proof: Proof. split. - apply of_inj. - intros E. rewrite <- of_hexadecimal_dnorm, E. apply of_hexadecimal_dnorm. Qed.
imports: Decimal DecimalFacts Hexadecimal HexadecimalFacts HexadecimalPos HexadecimalZ HexadecimalQ Rdefinitions