proposition: Lemma L_rec (X : {set A}) x y z : L^(z |: X) x y =i plus (conc (L^X x z) (conc (star (L^X z z)) (L^X z y))) (L^X x y).
proof: Proof. move => w. apply/idP/idP. - move: w x y. apply: (size_induction (measure := size)) => w IHw x y. move/L_split => [|[w1 [w2 [Hw' H1 Hw1 Hw2]]]]. + rewrite inE => ->. by rewrite orbT. + move: (IHw w2 H1 z y Hw2) Hw' => H4 -> {IHw H1}. rewrite inE (conc_cat Hw1 _) //. case/plusP : H4 => H; last by rewrite -[w2]cat0s conc_cat //. move/concP : H => [w21] [w22] [W1 [W2]] /concP [w221] [w222] [W3 [W4 W5]]; subst. by rewrite catA conc_cat // star_cat. - case/plusP ; last exact: L_monotone. move/concP => [w1] [w2] [-> [Hw1]] /concP [w3] [w4] [-> [Hw3 Hw4]]. by rewrite (L_catL Hw1) // (L_catR _ Hw4) // L_star. Qed.
imports: HB(structures) mathcomp(all_ssreflect) RegLang(setoid_leq misc languages dfa nfa)