proposition: Lemma to_hexadecimal_inj q q' : to_hexadecimal q <> None -> to_hexadecimal q = to_hexadecimal q' -> q = q'.
proof: Proof. intros Hnone EQ. generalize (of_to q) (of_to q'). rewrite <-EQ. revert Hnone; case to_hexadecimal; [|now simpl]. now intros d _ H1 H2; rewrite <-(H1 d eq_refl), <-(H2 d eq_refl). Qed.
imports: Decimal DecimalFacts Hexadecimal HexadecimalFacts HexadecimalPos HexadecimalZ HexadecimalQ Rdefinitions