proposition: Lemma open_gt : forall y : R, open (fun u : R => y < u).
proof: Proof. intros y x Hxy. apply Rminus_lt_0 in Hxy. exists (mkposreal _ Hxy). intros z Bz. replace y with (x - (x - y)) by ring. apply Rabs_lt_between'. apply Bz. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub