proposition: Lemma natn n : n%:R%R = n :> nat.
proof: Proof. by elim: n => // n; rewrite mulrS => ->. Qed.
imports: elpi(elpi) Coq(QArith) Coq.micromega(OrderedRing RingMicromega) mathcomp(all_ssreflect ssralg ssrnum ssrint) mathcomp.zify(ssrZ zify)