proposition: Lemma included_FDiv : included R P -> included R Q -> (forall x, R x -> forall Hx, G x Hx [#] [0]) -> included R (Dom Fdiv).
proof: Proof. intros HP HQ Hx. simpl in |- *. apply included_conj. assumption. unfold extend in |- *. split. apply HQ; assumption. intros; apply Hx; assumption. Qed.
imports: CoRN.algebra.CRings