proposition: Lemma anti_literals_valid_lit l : valid_lit l -> all valid_lit (anti_literals l).
proof: Proof. case: l => [] [x y] z /andP[/= Hz /andP[/= Hx Hy]]; rewrite !all_cat. apply/and3P; split; apply/allP => i /mapP [j]; rewrite mem_filter => /andP[Hd Hj] ->; apply/andP; split => //=. - by apply/andP; split=> //=; rewrite mem_iota in Hj. - by apply/andP; split=> //=; rewrite mem_iota in Hj. rewrite mem_cross in Hj; case/andP: Hj => Hj1 Hj2. apply: valid_get_rect_rev=> //. by rewrite ltn_divLR 1?mulnC ?Hx //; lia. rewrite ltn_divLR ?Hy //; lia. Qed.
imports: mathcomp(all_ssreflect) mathcomp(zify)