proposition: Lemma false_Req : forall x y : R, Reqb x y = false -> x <> y.
proof: Proof. intros. destruct (Req_dec x y). rewrite (Req_true x y e) in H. assert (H1 : true <> false). auto with *. contradiction. apply n. Qed.
imports: Lra Coq.Reals.Reals Reals.ROrderedType Notations