proposition: Lemma mem_merge_sudoku gs1 gs2 : merge_sudoku gs1 gs2 =i (gs1 ++ gs2).
proof: Proof. elim: gs2 gs1 => /= [[|a gs1]|a gs2 IH gs1 i] //=; first by rewrite cats0. by rewrite mem_insert_sudoku !(mem_cat, in_cons, IH); case: eqP => //; case: (_ \in _). Qed.
imports: mathcomp(all_ssreflect) mathcomp(zify)