proposition: Lemma suppCD L C C' : suppC L C' -> suppC L (C `\` C') -> suppC L C.
proof: Proof. move/allP => S1 /allP S2. apply/allP => s inC. case (boolP (s \in C')) => inC'; auto. apply: S2. by rewrite inE; bcase. Qed.
imports: mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert)