proposition: Lemma Sup_seq_scal_l (a : R) (u : nat -> Rbar) : 0 <= a -> Sup_seq (fun n => Rbar_mult a (u n)) = Rbar_mult a (Sup_seq u).
proof: Proof. case => Ha. rewrite /Sup_seq. case: ex_sup_seq => al Hau. case: ex_sup_seq => l Hu. simpl proj1_sig. apply Rbar_le_antisym. apply is_sup_seq_lub in Hau. apply is_sup_seq_lub in Hu. apply Hau => _ [n ->]. suff : Rbar_le (u n) l. case: (u n) => [un | | ] ; case: (l) => [l' | | ] /= ; try (by case) ; try (case: Rle_dec (Rlt_le _ _ Ha) => //= Ha' _ ; case: Rle_lt_or_eq_dec (Rlt_not_eq _ _ Ha) => //= _ _ _ ; by left). intros H ; apply Rmult_le_compat_l => // ; by apply Rlt_le. apply Hu. by exists n. suff : Rbar_le l (Rbar_div_pos al (mkposreal a Ha)). case: (al) => [al' | | ] ; case: (l) => [l' | | ] /= ; try (by case) ; try (case: Rle_dec (Rlt_le _ _ Ha) => //= Ha' _ ; case: Rle_lt_or_eq_dec (Rlt_not_eq _ _ Ha) => //= _ _ _ ; by left). intros H ; rewrite Rmult_comm ; apply Rle_div_r => //. apply is_sup_seq_lub in Hau. apply is_sup_seq_lub in Hu. apply Hu => _ [n ->]. suff : Rbar_le (Rbar_mult a (u n)) al. case: (u n) => [un | | ] ; case: (al) => [al' | | ] /= ; try (by case) ; try (case: Rle_dec (Rlt_le _ _ Ha) => //= Ha' _ ; case: Rle_lt_or_eq_dec (Rlt_not_eq _ _ Ha) => //= _ _ ; try (by case) ; by left). intros H ; rewrite Rmult_comm in H ; apply Rle_div_r => //. apply Hau. by exists n. rewrite -Ha. transitivity (Sup_seq (fun _ => 0)). apply Sup_seq_ext. move => n ; case: (u n) => [un | | ] /=. apply f_equal ; ring. case: Rle_dec (Rle_refl 0) => //= H _. case: Rle_lt_or_eq_dec (Rle_not_lt _ _ H) => //= H _. case: Rle_dec (Rle_refl 0) => //= H _. case: Rle_lt_or_eq_dec (Rle_not_lt _ _ H) => //= H _. transitivity 0. apply is_sup_seq_unique. move => eps ; split => /=. move => _ ; ring_simplify ; by apply eps. exists 0%nat ; apply Rminus_lt_0 ; ring_simplify ; by apply eps. case: (Sup_seq u) => [l | | ] /=. apply f_equal ; ring. case: Rle_dec (Rle_refl 0) => //= H _. case: Rle_lt_or_eq_dec (Rle_not_lt _ _ H) => //= H _. case: Rle_dec (Rle_refl 0) => //= H _. case: Rle_lt_or_eq_dec (Rle_not_lt _ _ H) => //= H _. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lub Markov Hierarchy