proposition: Lemma nat_sat {m n} : (map (fun i => m + i) (tower m n)) ++ (repeat 0 (4^n)) ~p [m*n] ++ (tower m n) ++ (tower m n) ++ (tower m n) ++ (tower m n).
proof: Proof. elim: n; first by rewrite Nat.mul_0_r. move=> n IH /=. rewrite ?map_app ?repeat_app /= app_nil_r. pose L := (map (fun i => m + i) (tower m n)) ++ (repeat 0 (4^n)). pose R := [m*n] ++ (tower m n) ++ (tower m n) ++ (tower m n) ++ (tower m n). have -> : m + m * n = m * (S n) by nia. apply: (Permutation_trans (l' := (L ++ L ++ L ++ L) ++ [m * S n])). { rewrite /L. by Permutation_trivial. } apply /Permutation_sym /(Permutation_elt [] _ _ []). rewrite /L IH. by Permutation_trivial. Qed.
imports: Arith Lia List Permutation Undecidability.SetConstraints.FMsetC Undecidability.SetConstraints.Util.Facts Undecidability.Synthetic.Definitions ssreflect ssrbool ssrfun