proposition: Lemma inclus_union_disj : forall a b c d : Ensf, inclus a c -> inclus b d -> inclus (union_disj a b) (union_disj c d).
proof: Proof. unfold inclus in |- *. intros. unfold union_disj in H1. cut (dans x (map injgauche a) \/ dans x (map injdroite b)); auto. intro Ht; elim Ht; clear Ht. intro. cut (exists y : Elt, dans y a /\ x = injgauche y). 2: apply dans_map; auto. intro Ht; elim Ht; clear Ht. intros y Ht; elim Ht; clear Ht; intros H3 H4. cut (dans y c); auto. intro. unfold union_disj in |- *. apply union_g. rewrite H4. apply dans_map_inv; auto. intro. cut (exists y : Elt, dans y b /\ x = injdroite y :>Elt). 2: apply dans_map; auto. intro Ht; elim Ht; clear Ht. intros y Ht; elim Ht; clear Ht; intros H3 H4. cut (dans y d); auto. intro. unfold union_disj in |- *. apply union_d. rewrite H4. apply dans_map_inv; auto. Qed.
imports: Ensf_types Ensf_dans Ensf_union Ensf_couple Ensf_inclus Ensf_map