proposition: Lemma sudoku_refine_id g1 g2 : sudoku g1 -> refine g1 g2 -> g1 = g2.
proof: Proof. move=> Hs /refineP[Hr1 Hr2 Hr3]. apply: (@eq_from_nth _ out) => [|i iLs1]; first by rewrite Hr2. rewrite Hr1 in iLs1. rewrite -[i]pos2nK //. have hw_pos : 0 < hw by case: hw iLs1. have Hv : valid_pos (n2pos i). by rewrite /valid_pos ltn_divLR ?iLs1 //= ltn_mod. apply: Hr3 => //. by have /sudoku_def[_ ->] := Hs. Qed.
imports: mathcomp(all_ssreflect) mathcomp(zify)