proposition: Lemma ders2der : forall E F, (forall x, Prod (set_pair_ders E F) bT x -> Prod (set_pair_der E F) bT x).
proof: Proof. rewrite /set_pair_ders /set_pair_der => E F [[e f] u] [[s -> ->] _]. split => //. by exists s; reflexivity. Qed.
imports: Coq(RelationClasses) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegLang(languages) RegexpBrzozowski(glue gfinset regexp finite_der)