proposition: Lemma sub_not_empty : forall l l', sub l l' -> lminus l' l <> [::].
proof: Proof. move => l l'. move/sub_elim => [ _ [a h1 h2] ] heq. have h : (InA (lminus l' l) a). rewrite lminusE. by apply/andP; split. move: h. by rewrite heq. Qed.
imports: Coq(RelationClasses Setoid Morphisms SetoidList Mergesort Permutation) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegexpBrzozowski(glue)