proposition: Lemma glb_eq_mult: forall (k : U) (f : natO -m> UI), glb (Imon (UMult k) @ f) == k * glb f.
proof: Proof. unfold glb; intros; auto. apply Oeq_trans with ([1-] lub (UPlus <_> ([1-]k) @ (UMult k @ (UInv @ f)))). apply Uinv_eq_compat; apply lub_eq_compat; apply fmon_eq_intro; simpl; auto. rewrite lub_eq_plus_cte_right. rewrite (lub_eq_mult k). apply Uinv_eq_perm_left; auto. rewrite Udistr_inv_left; auto. Qed.
imports: ALEA(Utheory)