proposition: Lemma filterlim_Rbar_mult_r : forall (a : R) (l : Rbar), filterlim (fun x => Rmult x a) (Rbar_locally l) (Rbar_locally (Rbar_mult l a)).
proof: Proof. intros a l. apply (filterlim_ext (fun x => a * x)). apply Rmult_comm. rewrite Rbar_mult_comm. apply filterlim_Rbar_mult_l. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lub Markov Hierarchy