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