proposition: Lemma P_automata_2 : P_automata -> Transition.
proof: Proof. unfold P_automata in |- *. intro temp; elim temp; clear temp. intros H temp; elim temp; clear temp. auto. Qed.
imports: Ensf Max Words fonctions need Relations