proposition: Lemma memPn A x : reflect {in A, forall y, y != x} (x \notin A).
proof: Proof. apply: (iffP idP) => [notDx y | notDx]; first by apply: contraTneq => ->. exact: contraL (notDx x) _. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool)