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