proposition: Lemma R_size_high n : R_size_rec n <= c * 4^(2 * n).
proof: Proof. elim: n => //= [|n IH]. - by rewrite mulnS muln0 addn0. - rewrite [in X in _^X]mulnS expnD mulnA [c * _]mulnC -mulnA. rewrite -(leqRW IH) -[4^2]/((1+3) * 4) -mulnA mulnDl mul1n leq_add //. by rewrite -(leqRW (R_size_low _)). Qed.
imports: HB(structures) mathcomp(all_ssreflect) RegLang(setoid_leq misc languages dfa nfa)