proposition: Lemma re_to_nfa_size e : #|re_to_nfa e| <= 2 * re_size e.
proof: Proof. elim: e; rewrite /= ?card_unit ?card_bool => //. - move => e IH. by rewrite card_option (leqRW IH) mulnS add2n. - move => e1 IH1 e2 IH2. by rewrite card_sum (leqRW IH1) (leqRW IH2) mulnS mulnDr add2n ltnW. - move => e1 IH1 e2 IH2. by rewrite card_sum (leqRW IH1) (leqRW IH2) mulnS mulnDr add2n ltnW. Qed.
imports: HB(structures) mathcomp(all_ssreflect) RegLang(setoid_leq misc languages dfa nfa)