proposition: Lemma Cheminmonoid : forall (w : Word) (q qd qa d : Ensf), automate q qd qa d -> forall e1 e2 : Elt, chemin e1 e2 q d w -> inmonoid alph w.
proof: Proof. simple induction w. auto. intros x w0 H q qd qa d H0 e1 e2 H1. cut (Chemin e1 e2 q d (cons x w0)); auto. intro. cut (exists e : Elt, chemin e e2 q d w0 /\ dans e1 q /\ dans x alph /\ dans (couple e1 (couple x e)) d); auto. intro H3; elim H3; clear H3. intros e H3; elim H3; clear H3. intros H3 H4; elim H4; clear H4. intros H4 H5; elim H5; clear H5; intros. apply inmonoid_cons; auto. apply (H q qd qa d H0 e e2); auto. Qed.
imports: Ensf Max Words Dec