proposition: Lemma to_of (d:int)(p:positive) : Pos.of_hex_int d = Some p -> Pos.to_hex_int p = norm d.
proof: Proof. unfold Pos.of_hex_int. destruct d; [ | intros [=]]. simpl norm. rewrite <- Unsigned.to_of. destruct (Pos.of_hex_uint d); now intros [= <-]. Qed.
imports: Hexadecimal HexadecimalFacts PArith NArith