proposition: Lemma negE C s : (s \in negatives C) = (s^- \in C).
proof: Proof. apply/fimsetP/idP => [ [[t [|]]] | H]. - by rewrite inE /= andbC. - by rewrite inE /negative andbT => ? ->. - exists (s^-) => //. by rewrite inE. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert sltype)