proposition: Lemma Uglb_eq_mult: forall (k : U) (f : nat -> U), Uglb (fun n => k * f n) == k * Uglb f.
proof: Proof. unfold Uglb; intros; auto. apply Oeq_trans with ([1-] Ulub (fun n => (k * [1-]f n) + [1-]k)). apply Uinv_eq_compat; apply Ulub_eq_compat; apply ford_eq_intro; simpl; auto. apply Oeq_trans with ([1-](Ulub (fun n => k * [1-]f n) + [1-]k)); auto. apply Oeq_trans with ([1-](k * Ulub (fun n => [1-]f n) + [1-]k)); auto. apply Uinv_eq_perm_left; auto. apply Oeq_trans with (k* [1-][1-](Ulub (fun n => [1-]f n)) + [1-]k); auto. Qed.
imports: ALEA(Utheory)