proposition: Lemma mem_insert_sudoku g gs : insert_sudoku g gs =i (g :: gs).
proof: Proof. elim: gs => //= g1 gs IH. case: grid_leqn (@grid_leqn_anti g g1) => [|_ i]. by case: grid_leqn => [->// i|_ i]; rewrite !in_cons; case: eqP. by rewrite !in_cons IH; do 2 case: eqP => //=. Qed.
imports: mathcomp(all_ssreflect) mathcomp(zify)