proposition: Lemma included_FRecip : included R Q -> (forall x, R x -> forall Hx, G x Hx [#] [0]) -> included R (Dom Frecip).
proof: Proof. intros H H0. simpl in |- *. unfold extend in |- *. split. apply H; assumption. intros; apply H0; assumption. Qed.
imports: CoRN.algebra.CRings