proposition: Lemma of_to (p:positive) : Pos.of_hex_uint (Pos.to_hex_uint p) = Npos p.
proof: Proof. unfold Pos.to_hex_uint. rewrite of_lu_rev. induction p; simpl; trivial. - now rewrite of_lu_succ_double, IHp. - now rewrite of_lu_double, IHp. Qed.
imports: Hexadecimal HexadecimalFacts PArith NArith