proposition: Lemma classic_sigW T (P : T -> Prop) : classically (exists x, P x) <-> classically (sig P).
proof: Proof. by split; apply: classic_bind => -[x Px]; apply/classicW; exists x. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra all_solvable) mathcomp(all_field)