proposition: Lemma fconj_continuous2 : forall A, continuous2 (Fconj A).
proof: Proof. intros; apply continuous2_sym. intros; repeat rewrite Fconj_simpl. apply fconj_sym. red; intros. rewrite Fconj_simpl. intro x. unfold fconj. unfold MF; repeat rewrite fcpo_lub_simpl. rewrite (Umult_right_continuous (k x) (h <o> x)). apply lub_le_compat; simpl; auto. Qed.
imports: ALEA(Utheory)