proposition: Lemma collb_trans : transitive collb.
proof: Proof. move => x y z /collP H1 /collP H2. apply/collP => w. by rewrite H1 H2. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph finfun finset generic_quotient) RegLang(misc languages dfa)