proposition: Lemma invariant_nil_refine_not_sudoku p st n g g1 : invariant ((n, p, [::]) :: st) g -> refine g g1 -> ~ sudoku g1.
proof: Proof. move=> Hs Hr Hsu. have [/= /andP[H1vs H2v3] H3vs H4vs] : valid_state ((n, p, [::]) :: st) by case: Hs. have Hp : valid_pos p by apply: H3vs; rewrite /= in_cons eqxx. have /= : in_state p (get p g1) ((n, p, [::]) :: st). apply: invariant_refine_update (Hs) _ _ _ _ => //. by case: Hs => _ _ -> //; rewrite in_cons eqxx. rewrite eqxx /in_val nth_nil /=. elim: (st) H1vs => //= [] [[n1 p1] v1] st1 IH. rewrite in_cons negb_or => /andP[/negPf-> Hpp] /=. by apply: IH. Qed.
imports: mathcomp(all_ssreflect) mathcomp(zify)