proposition: Lemma drinker : exists x, P x -> forall y, P y.
proof: Proof. case: (EM (exists y, ~P y)) => [[y notPy]| nonotPy]; first by exists y. exists d => _ y; case: (EM (P y)) => // notPy. by case: nonotPy; exists y. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div)