proposition: Lemma of_uint_acc_spec n d : Nat.of_hex_uint_acc d n = of_lu (rev d) + n * 0x10^usize d.
proof: Proof. revert n. induction d; intros; simpl Nat.of_hex_uint_acc; rewrite ?Nat.tail_mul_spec, ?IHd; simpl rev; simpl usize; rewrite ?Nat.pow_succ_r'; [ simpl; now rewrite Nat.mul_1_r | .. ]; unfold rev at 2; simpl revapp; rewrite of_lu_revapp; simpl of_lu; ring. Qed.
imports: Hexadecimal HexadecimalFacts Arith