proposition: Lemma square_spec_aux {n m A C} : C ++ (n :: A) ~p (repeat 0 (S m)) ++ (map S A) -> exists A', A ~p (seq 0 n) ++ A' /\ C ++ A' ~p (repeat 0 m) ++ (map S A').
proof: Proof. elim: n A. { move=> A /= /Permutation_sym /(@Permutation_cons_app_inv nat) /Permutation_sym H. by exists A. } move=> n IH A /[dup] /(Permutation_in (S n)). apply: unnest. { apply /in_app_iff => /=. tauto. } case /in_app_iff. { by move=> /(@repeat_spec nat). } move=> /in_map_iff [?] [[->]] /(@in_split nat) [A1 [A2 ?]]. subst A. move=> /(Permutation_trans _ (l := S n :: (C ++ (n :: (A1 ++ A2))))). apply: unnest. { by Permutation_trivial. } move=> /Permutation_sym /(Permutation_trans _ (l := S n :: ((repeat 0 (S m)) ++ map S (A1 ++ A2)))). apply: unnest. { rewrite !map_app /=. by Permutation_trivial. } move=> /Permutation_sym /(@Permutation_cons_inv nat) /IH [A' [? ?]]. exists A'. constructor; last done. rewrite seq_last -app_assoc. by apply: Permutation_elt. Qed.
imports: Arith Lia List Permutation Undecidability.SetConstraints.FMsetC Undecidability.SetConstraints.Util.Facts Undecidability.Synthetic.Definitions ssreflect ssrbool ssrfun