fact: Fixpoint Q_of_Rcst (r : Rcst) : Q := match r with | C0 => 0 # 1 | C1 => 1 # 1 | CZ z => z # 1 | CQ q => q | CPlus r1 r2 => Qplus (Q_of_Rcst r1) (Q_of_Rcst r2) | CMinus r1 r2 => Qminus (Q_of_Rcst r1) (Q_of_Rcst r2) | CMult r1 r2 => Qmult (Q_of_Rcst r1) (Q_of_Rcst r2) | CPow r1 z => Qpower (Q_of_Rcst r1) (z_of_exp z) | CInv r => Qinv (Q_of_Rcst r) | COpp r => Qopp (Q_of_Rcst r) end.
imports: OrderedRing QMicromega RingMicromega Refl Sumbool Raxioms Rfunctions RIneq Rpow_def QArith Qfield Qreals DeclConstant