proposition: Lemma R0_size x y : re_size (R0 x y) <= c.
proof: Proof. rewrite /= [X in X + _](_ : _ = 1); last by case (_ == _). rewrite add1n !ltnS. rewrite /edges -big_filter. apply: leq_trans (big_plus_size (m := 1) _) _ => [//|]. rewrite size_filter ltnS mulnC leq_mul2l /=. apply: leq_trans (count_size _ _) _. by rewrite /index_enum -enumT cardE. Qed.
imports: HB(structures) mathcomp(all_ssreflect) RegLang(setoid_leq misc languages dfa nfa)