proposition: Lemma N_of_hex_uint_accE (d : Hexadecimal.uint) (acc : positive) : N.pos (Pos.of_hex_uint_acc d acc) = N_of_hex_uint_acc d (N.pos acc).
proof: Proof. by elim: d acc => // d IHd acc; rewrite IHd 1?Pos.add_comm Pos.mul_comm. Qed.
imports: elpi(elpi) Coq(QArith) Coq.micromega(OrderedRing RingMicromega) mathcomp(all_ssreflect ssralg ssrnum ssrint) mathcomp.zify(ssrZ zify)