proposition: Lemma hex_uint_N_nat (d : Hexadecimal.uint) : nat_of_N (N.of_hex_uint d) = Nat.of_hex_uint d.
proof: Proof. rewrite N_of_hex_uintE /N_of_hex_uint /Nat.of_hex_uint. have ->: 0%N = nat_of_N 0%num by []. by elim: d 0%num => //= d IHd acc; rewrite IHd Nat.tail_mul_spec; congr Nat.of_hex_uint_acc; lia. Qed.
imports: elpi(elpi) Coq(QArith) Coq.micromega(OrderedRing RingMicromega) mathcomp(all_ssreflect ssralg ssrnum ssrint) mathcomp.zify(ssrZ zify)