proposition: Lemma large_nat_Z_int (n : large_nat) : int_of_Z (Z_of_large_nat n) = nat_of_large_nat n.
proof: Proof. rewrite -large_nat_N_nat; case: n => [n|[d|d]] //=; first lia. by rewrite /Z.of_uint /N.of_uint; lia. by rewrite /Z.of_hex_uint /N.of_hex_uint; lia. Qed.
imports: elpi(elpi) Coq(QArith) Coq.micromega(OrderedRing RingMicromega) mathcomp(all_ssreflect ssralg ssrnum ssrint) mathcomp.zify(ssrZ zify)