proposition: Lemma invariant_refine_update p st g g1 : invariant st g -> valid_pos p -> get p g \notin sref -> refine g g1 -> sudoku g1 -> in_state p (get p g1) st.
proof: Proof. move=> [Hs Hpos Hanti Hi [His1 His2]] Hv Hgp /refineP[H1r H2r H3r] /sudoku_def[H1su H2su H3su]. case: (boolP (in_state _ _ _)) => // Hz. case: (His2 p (get p g1)) => // [|p2 [H1p2 H2p2 H3p2]]. by apply: H2su. rewrite (H3r p2) // in H3p2. by have := H3su _ _ _ H1p2 H3p2; rewrite eqxx. Qed.
imports: mathcomp(all_ssreflect) mathcomp(zify)