proposition: Lemma QSORaddon : @SORaddon R R0 R1 Rplus Rmult Rminus Ropp (@eq R) Rle Q 0%Q 1%Q Qplus Qmult Qminus Qopp Qeq_bool Qle_bool Q2R nat to_nat pow.
proof: Proof. constructor. - constructor ; intros ; try reflexivity. + apply Q2R_0. + apply Q2R_1. + apply Q2R_plus. + apply Q2R_minus. + apply Q2R_mult. + apply Q2R_opp. + apply Qeq_true ; auto. - apply R_power_theory. - apply Qeq_false. - apply Qle_true. Qed.
imports: OrderedRing QMicromega RingMicromega Refl Sumbool Raxioms Rfunctions RIneq Rpow_def QArith Qfield Qreals DeclConstant