proposition: Lemma valid_pos_anti_literals p1 p2 z1 z2 : (p1, z1) \in anti_literals (p2, z2) -> valid_pos p2 -> valid_pos p1.
proof: Proof. case: p1 => x1 y1; case: p2 => x2 y2. rewrite !mem_cat => /or3P[] /mapP[x]; rewrite mem_filter ?mem_iota ?mem_cross ?add0n /= => /andP[Hd Hhw] [-> -> _] /andP[/= x2Lhw y2Lhw]; rewrite /valid_pos /=. - by rewrite x2Lhw Hhw. - by rewrite Hhw y2Lhw. have /andP[x1Lh x2Lw] := Hhw. by rewrite hw_divhMD // hw_divwMD. Qed.
imports: mathcomp(all_ssreflect) mathcomp(zify)