proposition: Lemma pyramid_shuffle {n} : seq 0 n ++ pyramid n ~p repeat 0 n ++ map S (pyramid n).
proof: Proof. elim: n; first done. move=> n IH. rewrite /pyramid seq_last /plus flat_map_concat_map map_app concat_app. rewrite -flat_map_concat_map -/(pyramid _) ? map_app /= ? app_nil_r seq_shift. apply: (Permutation_trans (l' := (seq 0 n ++ [n]) ++ (seq 0 n ++ pyramid n))). { by Permutation_trivial. } rewrite IH -seq_last /=. by Permutation_trivial. Qed.
imports: Arith Lia List Permutation Undecidability.SetConstraints.FMsetC Undecidability.SetConstraints.Util.Facts Undecidability.Synthetic.Definitions ssreflect ssrbool ssrfun