proposition: Lemma limsup_eq_mult : forall k (f : nat -> U), limsup (fun n => k * f n) == k * limsup f.
proof: Proof. unfold limsup; intros. apply Oeq_trans with (glb (Imon (UMult k) @ (Fsup f))); auto. apply glb_eq_compat; apply fmon_eq_intro; simpl; unfold fsup; intros; auto. rewrite glb_eq_mult; trivial. Qed.
imports: ALEA(Utheory)