proposition: Lemma absurd_injg_injd : forall (x : Elt) (e f : Ensf), dans x (map injgauche e) -> ~ dans x (map injdroite f).
proof: Proof. intros. cut (exists y : Elt, dans y e /\ x = injgauche y). 2: apply dans_map; auto. intro Ht; elim Ht; clear Ht. intros y Ht; elim Ht; clear Ht. intros. red in |- *. intro. cut (exists y' : Elt, dans y' f /\ x = injdroite y' :>Elt). 2: apply dans_map; auto. intro Ht; elim Ht; clear Ht. intros y' Ht; elim Ht; clear Ht. intros. absurd (zero = un :>Elt). unfold zero in |- *. unfold un in |- *. discriminate. unfold injdroite in H4. unfold injgauche in H1. replace zero with (second (couple y zero)); auto. replace un with (second (couple y' un)); auto. rewrite <- H4. rewrite <- H1. auto. Qed.
imports: Ensf_types Ensf_dans Ensf_union Ensf_couple Ensf_inclus Ensf_map