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