proposition: Lemma to_uint_pos_surj d : unorm d<>zero -> exists p, Pos.to_hex_uint p = unorm d.
proof: Proof. intros. destruct (Pos.of_hex_uint d) eqn:E. - destruct H. generalize (to_of d). now rewrite E. - exists p. generalize (to_of d). now rewrite E. Qed.
imports: Hexadecimal HexadecimalFacts PArith NArith