proposition: Lemma Qeq_true : forall x y, Qeq_bool x y = true -> Q2R x = Q2R y.
proof: Proof. intros. now apply Qeq_eqR, Qeq_bool_eq. Qed.
imports: OrderedRing QMicromega RingMicromega Refl Sumbool Raxioms Rfunctions RIneq Rpow_def QArith Qfield Qreals DeclConstant