proposition: Lemma flipcl_refl F s : s \in F -> forall b, (s, b) \in flipcl F.
proof: Proof. move => inF [|]; apply/cupP; exists s; by rewrite inF /= !inE. Qed.
imports: Relations Lia Setoid Morphisms mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert sltype rewrite_inequality fset_tac)