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