proposition: Lemma anti_literals_nswap p1 p2 z1 z2 : valid_pos p2 -> (p2, z2) \notin anti_literals (p1, z1) -> (p1, z1) \notin anti_literals (p2, z2).
proof: Proof. by move=> Hp2; apply/contra/anti_literals_swap. Qed.
imports: mathcomp(all_ssreflect) mathcomp(zify)