proposition: Lemma square_spec {n A} : (seq 0 n) ++ A ~p (repeat 0 n) ++ (map S A) -> length A + length A + n = n * n.
proof: Proof. elim: n A. { move=> A /Permutation_sym /Permutation_map_lt_nil ->; by [|lia]. } move=> n IH A. rewrite seq_last. rewrite -app_assoc. move=> /square_spec_aux [A' [/Permutation_length + /IH]]. rewrite app_length seq_length. by lia. Qed.
imports: Arith Lia List Permutation Undecidability.SetConstraints.FMsetC Undecidability.SetConstraints.Util.Facts Undecidability.Synthetic.Definitions ssreflect ssrbool ssrfun