proposition: Lemma transition_a_gauche_2 : forall (q1 qa1 d1 q2 qd2 d2 : Ensf) (e0 x e : Elt), dans e0 (map injgauche q1) -> dans x alph -> dans (couple e0 (couple x e)) (union (pont qa1 qd2) (union (injg_d1 q1 d1) (injd_d2 q2 d2))) -> dans (couple (first e0) (couple x (first e))) d1.
proof: Proof. intros. cut (dans (couple e0 (couple x e)) (pont qa1 qd2) \/ dans (couple e0 (couple x e)) (union (injg_d1 q1 d1) (injd_d2 q2 d2))); auto. intro Ht; elim Ht; clear Ht. unfold pont in |- *. intro. cut (exists y : Elt, dans y (prodcart qa1 qd2) /\ couple e0 (couple x e) = transition_pont y :>Elt). 2: apply dans_map; auto. intro Ht; elim Ht; clear Ht; intros y Ht; elim Ht; clear Ht; intros H3 H4. cut (exists y1 : Elt, (exists y2 : Elt, dans y1 qa1 /\ dans y2 qd2 /\ y = couple y1 y2 :>Elt)). 2: apply coupl3; auto. intro Ht; elim Ht; clear Ht; intros y1 Ht; elim Ht; clear Ht; intros y2 Ht; elim Ht; clear Ht; intros H5 Ht; elim Ht; clear Ht; intros H6 H7. cut (couple e0 (couple x e) = transition_pont (couple y1 y2) :>Elt). 2: rewrite <- H7; auto. unfold transition_pont in |- *. intro. cut (couple x e = couple epsilon (couple y2 un) :>Elt). 2: apply couple_couple_inv2 with e0 (couple y1 zero); auto. intro. cut (x = epsilon :>Elt). 2: apply couple_couple_inv1 with e (couple y2 un); auto. intro. absurd (dans x alph); auto. rewrite H10. red in |- *; intro; apply not_dans_epsilon_alph; assumption. intro. clear H1. cut (dans (couple e0 (couple x e)) (injg_d1 q1 d1) \/ dans (couple e0 (couple x e)) (injd_d2 q2 d2)); auto. intro Ht; elim Ht; clear Ht. unfold injg_d1 in |- *. intro. cut (dans (couple e0 (couple x e)) (prodcart (map injgauche q1) (prodcart alph (map injgauche q1))) /\ est_dans_d' d1 (couple e0 (couple x e))). 2: apply dans_tq_imp; auto. intro Ht; elim Ht; clear Ht; intros. auto. unfold injd_d2 in |- *. intro. cut (dans (couple e0 (couple x e)) (prodcart (map injdroite q2) (prodcart alph (map injdroite q2))) /\ est_dans_d' d2 (couple e0 (couple x e))). 2: apply dans_tq_imp; auto. intro Ht; elim Ht; clear Ht; intros. cut (dans e0 (map injdroite q2) /\ dans (couple x e) (prodcart alph (map injdroite q2))). 2: apply coupl2; auto. intro Ht; elim Ht; clear Ht; intros. absurd (dans e0 (map injdroite q2)); auto. apply absurd_injg_injd with q1; auto. Qed.
imports: Ensf Max Words Dec Reg Rat