proposition: Lemma seq_sat2 {d n} : let A n := map (fun i => (S d) * i) (seq 0 n) in (A n) ++ [(S d) * n] ~p [0] ++ (map (fun i => (S d) + i) (A n)).
proof: Proof. move=> A. elim: n. { apply: Permutation_refl'. congr cons. by lia. } move=> n IH. rewrite /A seq_last ?map_app -/(A n) /(map _ [n]) IH. have ->: S d * S n = S d + S d * n by lia. by Permutation_trivial. Qed.
imports: Arith Lia List Permutation Undecidability.SetConstraints.FMsetC Undecidability.SetConstraints.Util.Facts Undecidability.Synthetic.Definitions ssreflect ssrbool ssrfun