proposition: Lemma to_int_inj n n' : N.to_hex_int n = N.to_hex_int n' -> n = n'.
proof: Proof. intro E. assert (E' : Some n = Some n'). { now rewrite <- (of_to n), <- (of_to n'), E. } now injection E'. Qed.
imports: Hexadecimal HexadecimalFacts HexadecimalPos PArith NArith