proposition: Lemma fmult_continuous2 : forall A, continuous2 (Fmult A).
proof: Proof. red; intros. rewrite Fmult_simpl. intro x; unfold fmult. unfold MF; repeat rewrite fcpo_lub_simpl. rewrite (Umult_continuous2 f (g <o> x)). apply lub_le_compat; intro y; simpl; auto. Qed.
imports: ALEA(Utheory)