proposition: Lemma all_notin (p : pred A) xs y : all p xs -> ~~ p y -> y \notin xs.
proof: Proof. by move/allP=>Ha; apply/contra/Ha. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq eqtype path fintype finfun tuple interval perm fingroup) pcm(options prelude ordtype seqext slice)