proposition: Lemma nat_spec {n A B C} : (map S B) ++ A ~p [n] ++ B ++ B ++ B ++ B -> (map S (map S C)) ++ A ~p [2*n] ++ C ++ C ++ C ++ C -> Forall (fun a => 0 = a) A.
proof: Proof. have eval_map p' A' : eval p' (map S A') = p' * eval p' A'. { rewrite /eval. elim: A'; first done. move=> > /= ->. by nia. } move=> /(eval_eq (p := 4)) + /(eval_eq (p := 2)). rewrite /eval !map_app !list_sum_app -!/(eval _ _) !eval_map. have -> : eval 2 [2 * n] = eval 4 [n]. { have := Nat.pow_mul_r 2 2 n. rewrite /eval /=. lia. } move=> ??. have : not (eval 2 A < eval 4 A) by lia. by have /(eval_monotone (A := A)) [] : 2 < 4 by lia. Qed.
imports: Arith Lia List Permutation Undecidability.SetConstraints.FMsetC Undecidability.SetConstraints.Util.Facts Undecidability.Synthetic.Definitions ssreflect ssrbool ssrfun