proposition: Lemma is_LimSup_seq_const (a : R) : is_LimSup_seq (fun _ => a) a.
proof: Proof. intros eps ; split. intros N ; exists N ; split. by apply Nat.le_refl. apply Rminus_lt_0 ; ring_simplify. by apply eps. exists O => _ _. apply Rminus_lt_0 ; ring_simplify. by apply eps. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lub Markov Hierarchy