fact: Definition Qeval_nformula := eval_nformula 0 Rplus Rmult (@eq R) Rle Rlt Q2R.
imports: OrderedRing QMicromega RingMicromega Refl Sumbool Raxioms Rfunctions RIneq Rpow_def QArith Qfield Qreals DeclConstant EnvRing