proposition: Lemma to_hexadecimal_surj d : exists q, to_hexadecimal q = Some (dnorm d).
proof: Proof. exists (of_hexadecimal d). apply to_of. Qed.
imports: Decimal DecimalFacts Hexadecimal HexadecimalFacts HexadecimalPos HexadecimalZ HexadecimalQ Rdefinitions