proposition: Lemma Inf_seq_scal_l (a : R) (u : nat -> Rbar) : 0 <= a -> Inf_seq (fun n => Rbar_mult a (u n)) = Rbar_mult a (Inf_seq u).
proof: Proof. move => Ha. rewrite Inf_opp_sup. rewrite -(Sup_seq_ext (fun n => Rbar_mult a (Rbar_opp (u n)))). rewrite Sup_seq_scal_l. by rewrite -Rbar_mult_opp_r -(Inf_opp_sup u). by []. move => n ; by rewrite Rbar_mult_opp_r. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lub Markov Hierarchy