proposition: Lemma eval_monotone {p q A} : p < q -> eval p A < eval q A \/ Forall (fun a => 0 = a) A.
proof: Proof. move=> Hpq. elim: A; first by right. rewrite /eval. move=> [|n] A [IH|IH]. - left => /=. lia. - right. by constructor. - left. have := Nat.pow_lt_mono_l p q (S n) (Nat.neq_succ_0 n) Hpq. move=> /=. lia. - left. have := Nat.pow_lt_mono_l p q (S n) (Nat.neq_succ_0 n) Hpq. move=> /= ?. have -> : list_sum (map (Nat.pow p) A) = list_sum (map (Nat.pow q) A). { elim: A IH; first done. by move=> m A IH /Forall_cons_iff [<- /IH] /= ->. } by lia. Qed.
imports: Arith Lia List Permutation Undecidability.SetConstraints.FMsetC Undecidability.SetConstraints.Util.Facts Undecidability.Synthetic.Definitions ssreflect ssrbool ssrfun