proposition: Lemma rat_is_reg : forall L : wordset, isrationnal L -> isregular L.
proof: Proof. intros L H. elim H. intros; apply lword_is_reg; auto. intros; apply lunion_is_reg; auto. intros; apply lconc_is_reg; auto. intros; apply lstar_is_reg; auto. Qed.
imports: Ensf Max Words Dec Reg Rat