proposition: Lemma of_hexadecimal_dnorm d : of_hexadecimal (dnorm d) = of_hexadecimal d.
proof: Proof. now apply to_hexadecimal_inj; rewrite !to_of; [|rewrite dnorm_involutive]. Qed.
imports: Decimal DecimalFacts Hexadecimal HexadecimalFacts HexadecimalPos HexadecimalZ HexadecimalQ Rdefinitions