proposition: Lemma invariant_nil g : invariant [::] g -> sudoku g.
proof: Proof. move=> [Hs Hpos Hanti Hi [His1 His2]]. apply/sudoku_def; split=> //. move=> p1 p2 z Hv Hz; apply/negP => /eqP Hg. have : (p1, get p1 g) \notin anti_literals (p2, get p2 g). apply: Hi => //. - by apply: valid_pos_anti_literals Hz _. - by rewrite Hanti. by rewrite Hg (eqz_anti_literals Hz) Hanti. rewrite Hg => /anti_literals_nswap => /(_ Hv). by case: (_ \in _) Hz. Qed.
imports: mathcomp(all_ssreflect) mathcomp(zify)