proposition: Lemma dans_pont_imp_epsilon : forall (qa1 qd2 : Ensf) (e1 x e0 : Elt), dans (couple e1 (couple x e0)) (pont qa1 qd2) -> x = epsilon :>Elt.
proof: Proof. intros qa1 qd2 e1 x e0. unfold pont in |- *. intro. cut (exists y : Elt, dans y (prodcart qa1 qd2) /\ couple e1 (couple x e0) = transition_pont y :>Elt). 2: apply dans_map; auto. intro Ht; elim Ht; clear Ht; intros y Ht; elim Ht; clear Ht; intros H0 H1. 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 H2 Ht; elim Ht; clear Ht; intros H3 H4. cut (couple e1 (couple x e0) = transition_pont (couple y1 y2) :>Elt). 2: rewrite <- H4; assumption. unfold transition_pont in |- *. intro. cut (couple x e0 = couple epsilon (couple y2 un) :>Elt). 2: apply couple_couple_inv2 with e1 (couple y1 zero); assumption. intro. apply couple_couple_inv1 with e0 (couple y2 un); assumption. Qed.
imports: Ensf Max Words Dec Reg Rat