proposition: Lemma liminf_eq_mult : forall k (f : nat -> U), liminf (fun n => k * f n) == k * liminf f.
proof: Proof. unfold liminf; intros. apply Oeq_trans with (lub ((UMult k) @ (Finf f))); auto. apply lub_eq_compat; apply fmon_eq_intro; simpl; unfold finf; intros; auto. Qed.
imports: ALEA(Utheory)