proposition: Lemma notin_anti_literals l : l \notin anti_literals l.
proof: Proof. case: l => [] [x y] z. rewrite !mem_cat !negb_or; apply/and3P; split; apply/negP=> /mapP. - by move=> [y1 Hy1 [yE]]; rewrite yE mem_filter eqxx in Hy1. - by move=> [x1 Hx1 [xE]]; rewrite xE mem_filter eqxx in Hx1. - move=> [[x2 y2] Hxy2 [xE yE]]. by rewrite mem_filter xpair_eqE /= -xE -yE !eqxx in Hxy2. Qed.
imports: mathcomp(all_ssreflect) mathcomp(zify)