proposition: Lemma Qeq_false : forall x y, Qeq_bool x y = false -> Q2R x <> Q2R y.
proof: Proof. intros. apply Qeq_bool_neq in H. contradict H. now apply eqR_Qeq. Qed.
imports: OrderedRing QMicromega RingMicromega Refl Sumbool Raxioms Rfunctions RIneq Rpow_def QArith Qfield Qreals DeclConstant