proposition: Lemma supp0F s : ~~ fset0 |> s.
proof: Proof. case: s => /=. elim => [|x|s IHs t IHt|s IHs|s IHs t IHt|s IHt t IHs] [|] //=; by rewrite ?inE // ?negb_or ?negb_and ?IHs ?IHt. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert sltype)