proposition: Lemma included_FMax : included R P -> included R Q -> included R (Dom (FMax F G)).
proof: Proof. intros; simpl in |- *; apply included_conj; assumption. Qed.
imports: CoRN.reals.Q_in_CReals Coq.QArith.Qabs CoRN.reals.CauchySeq