proposition: Lemma closed_flipcl F : flip_closed (flipcl F).
proof: Proof. move => s /cupP [t] /and3P [inF _ H]. apply/cupP. exists t. move: H. rewrite inF /= !inE. case/orP => /eqP -> /=; by rewrite eqxx. Qed.
imports: Relations Lia Setoid Morphisms mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert sltype rewrite_inequality fset_tac)