proposition: Lemma anti_literals_swap p1 p2 z1 z2 : valid_pos p1 -> (p2, z2) \in anti_literals (p1, z1) -> (p1, z1) \in anti_literals (p2, z2).
proof: Proof. case: p1 => x1 y1; case: p2 => x2 y2 => /andP[/= x1Lhw y1Lhw]. rewrite !mem_cat => /or3P[] /mapP[x]; rewrite mem_filter ?mem_iota ?mem_cross ?add0n => /andP[Hd Hhw] [-> -> ->]. - apply/or3P; apply: Or31. by rewrite map_f // mem_filter // eq_sym Hd mem_iota. - apply/or3P; apply: Or32. by rewrite map_f // mem_filter // eq_sym Hd mem_iota. apply/or3P; apply: Or33. have h_pos := h_pos x1Lhw; have w_pos := w_pos x1Lhw. have /andP[x1Lh x2Lw] := Hhw. rewrite !divnMDl // (divn_small x1Lh) (divn_small x2Lw) !addn0. have ->: (x1, y1) = shift (x1 %% h, y1 %% w) (x1 %/ h * h) (y1 %/ w * w). by rewrite /shift /= -!divn_eq. rewrite map_f // mem_filter mem_cross /= hw_modh // hw_modw // !andbT. rewrite /shift /= xpair_eqE {1}(divn_eq x1 h) {1}(divn_eq y1 w) !eqn_add2l eq_sym [_ == x.2]eq_sym in Hd. by rewrite /shift /= xpair_eqE /= !eqn_add2l. Qed.
imports: mathcomp(all_ssreflect) mathcomp(zify)