proposition: Lemma flip_drop_sign F s : s \in flipcl F -> drop_sign s \in F.
proof: Proof. case/cupP => t. case/and3P => inF _. rewrite !inE. case/orP; by move/eqP => ->. Qed.
imports: Relations Lia Setoid Morphisms mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert sltype rewrite_inequality fset_tac)