proposition: Lemma dans_map_trans : forall (x : Elt) (f : Elt -> Elt) (a b : Ensf), dans x (map f a) -> inclus a b -> dans x (map f b).
proof: Proof. intros. cut (exists y : Elt, dans y a /\ x = f y :>Elt). 2: apply dans_map; auto. intro Ht; elim Ht; clear Ht. intros y Ht; elim Ht; clear Ht. intros. cut (dans y b). 2: apply dans_trans with a; auto. intro. rewrite H2. apply dans_map_inv; auto. Qed.
imports: Ensf_types Ensf_dans Ensf_union Ensf_inclus