proposition: Lemma of_uint_acc_eqn d acc : d<>Nil -> Pos.of_hex_uint_acc d acc = Pos.of_hex_uint_acc (tl d) (Nadd (hd d) (0x10*acc)).
proof: Proof. destruct d; simpl; trivial. now destruct 1. Qed.
imports: Hexadecimal HexadecimalFacts PArith NArith