proposition: Lemma of_to (n:nat) : Nat.of_hex_int (Nat.to_hex_int n) = Some n.
proof: Proof. unfold Nat.to_hex_int, Nat.of_hex_int, norm. f_equal. rewrite Unsigned.of_uint_norm. apply Unsigned.of_to. Qed.
imports: Hexadecimal HexadecimalFacts Arith