proposition: Lemma N_of_uintE : N.of_uint =1 N_of_uint.
proof: Proof. rewrite /N.of_uint /Pos.of_uint /N_of_uint /=. by elim => //= d _; rewrite N_of_uint_accE. Qed.
imports: elpi(elpi) Coq(QArith) Coq.micromega(OrderedRing RingMicromega) mathcomp(all_ssreflect ssralg ssrnum ssrint) mathcomp.zify(ssrZ zify)