proposition: Lemma filterlim_Rbar_mult_l : forall (a : R) (l : Rbar), filterlim (Rmult a) (Rbar_locally l) (Rbar_locally (Rbar_mult a l)).
proof: Proof. intros a l. case: (Req_dec a 0) => [->|Ha]. apply (filterlim_ext (fun _ => 0)). intros x. apply sym_eq, Rmult_0_l. rewrite Rbar_mult_0_l. apply filterlim_const. eapply filterlim_comp_2. apply filterlim_const. apply filterlim_id. eapply (filterlim_Rbar_mult a l). apply Rbar_mult_correct ; by case: l. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lub Markov Hierarchy