proposition: Theorem not_exists_forall : excluded_middle -> forall (X: Type) (P : X -> Prop), ~ (exists x, ~ P x) -> (forall x, P x).
proof: Proof. move=> Em X P H x; rewrite /excluded_middle in Em. move: (Em (P x)); case=>// => H1. by suff: False =>//; apply:H; exists x. Qed.
imports: mathcomp(ssreflect)