proposition: Lemma classic_ex T (P : T -> Prop) : ~ (forall x, ~ P x) -> classically (ex P).
proof: Proof. move=> NfNP; apply/classicPT => exPF; apply: NfNP => x Px. by apply: exPF; exists x. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra all_solvable) mathcomp(all_field)