proposition: Lemma cart_inclus : forall a b c d : Ensf, inclus a b -> inclus c d -> inclus (prodcart a c) (prodcart b d).
proof: Proof. unfold inclus in |- *. intros. cut (exists x1 : Elt, (exists x2 : Elt, dans x1 a /\ dans x2 c /\ x = couple x1 x2)). 2: apply coupl3; auto. intro H2; elim H2; clear H2. intros x1 H2; elim H2; clear H2. intros x2 H2; elim H2; clear H2. intros H2 H3; elim H3; clear H3. intros H3 H4. rewrite H4. auto. Qed.
imports: Ensf_types Ensf_dans Ensf_union Ensf_produit