proposition: Lemma large_nat_N_nat (n : large_nat) : nat_of_N (N_of_large_nat n) = nat_of_large_nat n.
proof: Proof. case: n => [n|[d|d]] /=; first by rewrite nat_of_N_expandE; lia. by rewrite uint_N_nat. by rewrite hex_uint_N_nat. Qed.
imports: elpi(elpi) Coq(QArith) Coq.micromega(OrderedRing RingMicromega) mathcomp(all_ssreflect ssralg ssrnum ssrint) mathcomp.zify(ssrZ zify)