proposition: Lemma glb_eq_plus_cte_right: forall (f : natO -m> UI) (k : U), glb (Imon (UPlus <_> k) @ f) == glb f + k.
proof: Proof. unfold glb; intros. apply Oeq_trans with ([1-] lub (UEsp <_> ([1-]k) @ (UInv @ f))); auto. apply Uinv_eq_compat; apply lub_eq_compat; apply fmon_eq_intro; simpl; auto. apply Oeq_trans with ([1-] (lub (UInv @ f) & [1-] k)). apply Uinv_eq_compat; apply (lub_eq_esp_right (UInv @ f) ([1-]k)). rewrite Uinv_esp_plus; auto. Qed.
imports: ALEA(Utheory)