proposition: Lemma ldisjoint_lminus: forall l1 l2, ldisjoint l1 (lminus l2 l1).
proof: Proof. move => l1 l2; apply/ldisjointP => x hx. rewrite lminusE. case/andP => hn hx2. move/negP : hn. by apply. Qed.
imports: Coq(RelationClasses Setoid Morphisms SetoidList Mergesort Permutation) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegexpBrzozowski(glue)