proposition: Lemma nat_of_N_expandE : nat_of_N_expand = nat_of_N.
proof: Proof. by []. Qed.
imports: elpi(elpi) Coq(QArith) Coq.micromega(OrderedRing RingMicromega) mathcomp(all_ssreflect ssralg ssrnum ssrint) mathcomp.zify(ssrZ zify)