proposition: Lemma lub_eq_plus_cte_right : forall (f : natO -m> U) (k:U), lub ((UPlus <_> k) @ f) == lub f + k.
proof: Proof. intros; apply Oeq_trans with (k + lub f); auto. apply Oeq_trans with (lub (UPlus k @ f)); auto. apply lub_eq_compat; simpl; intros. apply fmon_eq_intro; simpl; intros. rewrite (Uplus_sym (f n) k); auto. Qed.
imports: ALEA(Utheory)