proposition: Lemma Y_false (P:Prop) (hyp : ~P) x y: Yo P x y = y.
proof: Proof. rewrite /Yo -lock /Yo_def. symmetry; apply: (select_uniq _ (set2_2 x y)); last by right. by move => u v _; case; case => // _ -> _; case; case => // _. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)