fact: Definition Reval_nformula : PolEnv R -> NFormula Z -> Prop := eval_nformula 0 +%R *%R eq <=%O <%O (fun n => (int_of_Z n)%:~R).
imports: elpi(elpi) Coq(QArith Ring) Coq.micromega(RingMicromega QMicromega EnvRing Tauto Lqa) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(fintype finfun bigop order ssralg ssrnum ssrint) mathcomp.zify(ssrZ zify) mathcomp.algebra_tactics(common)