proposition: Lemma lwordnil_is_reg2 : forall w : Word, reconnait (singleton zero) (singleton zero) (singleton zero) (prodcart empty (prodcart alph empty)) w -> w = nil :>Word.
proof: Proof. unfold reconnait at 1 in |- *. simple induction w. auto. intros x w0 H H0. clear H. elim H0; intros; clear H0. elim H1; intros; clear H1. elim H0; intros; clear H0. elim H1; intros; clear H1. elim H2; intros; clear H2. cut (Chemin x0 x1 (singleton zero) (prodcart empty (prodcart alph empty)) (cons x w0)). 2: auto. unfold Chemin in |- *; simpl in |- *. intro H2. absurd (dans x0 empty). auto. elim H2; intros; clear H2. elim H4; intros; clear H4. elim H5; intros; clear H5. elim H6; intros; clear H6. cut (dans x0 empty /\ dans (couple x x2) (prodcart alph empty)). 2: apply coupl2; assumption. tauto. Qed.
imports: Ensf Max Words Dec Reg Rat