proposition: Lemma glb_eq_plus_cte_left: forall (f : natO -m> UI) (k : U), glb (Imon (UPlus k) @ f) == k + glb f.
proof: Proof. intros; apply Oeq_trans with (glb f + k); auto. apply Oeq_trans with (glb (Imon (UPlus <_> k) @ f)); auto. apply glb_eq_compat; apply fmon_eq_intro; simpl; auto. Qed.
imports: ALEA(Utheory)