proposition: Fact power_decomp_lt n f a q : (forall i j, i < j < n -> f i < f j) -> (forall i, i < n -> f i < q) -> (forall i, i < n -> a i < p) -> ∑ n (fun i => a i * power (f i) p) < power q p.
proof: Proof. Proof using Hp. revert q; induction n as [ | n IHn ]; intros q Hf1 Hf2 Ha. + rewrite msum_0; apply power_ge_1; lia. + rewrite msum_plus1; auto. apply Nat.lt_le_trans with (1*power (f n) p + a n * power (f n) p). * apply Nat.add_lt_le_mono; auto. rewrite Nat.mul_1_l. apply IHn. - intros; apply Hf1; lia. - intros; apply Hf1; lia. - intros; apply Ha; lia. * rewrite <- Nat.mul_add_distr_r. replace q with (S (q-1)). - rewrite power_S; apply Nat.mul_le_mono; auto. ++ apply Ha; auto. ++ apply power_mono_l; try lia. generalize (Hf2 n); intros; lia. - generalize (Hf2 0); intros; lia. Qed.
imports: Arith Nat Lia Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd rel_iter sums)