proposition: Lemma R_size x : re_size (R^(enum A) (dfa_s A) x) <= R_size_rec #|A| .
proof: Proof. rewrite cardE. elim: (enum A) (dfa_s A) x => [|r s IH] p q. - exact: R0_size. - rewrite /= 6!(addSn,addnS) addn4 !ltnS !(leqRW (IH _ _)). by rewrite !mulSn mul0n addn0 !addnA. Qed.
imports: HB(structures) mathcomp(all_ssreflect) RegLang(setoid_leq misc languages dfa nfa)