proposition: Lemma SUB2 : forall r1 r2, SUB r1 r2 <-> r2 ≡ (Plus r1 r2).
proof: Proof. rewrite /SUB /EQUIV => r1 r2; split => h s. - rewrite -!topredE /=. apply/idP/orP. move => h'; by right. case => hu //. by apply: h. - rewrite (h s) -!topredE /= => h1. apply/orP. by left. Qed.
imports: Coq(RelationClasses) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegLang(languages) RegexpBrzozowski(glue gfinset regexp finite_der)