proposition: Lemma filter_le_trans : forall T F G H, @filter_le T F G -> filter_le G H -> filter_le F H.
proof: Proof. intros T F G H FG GH P K. now apply FG, GH. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub