proposition: Fact sum_powers_inc_lt_last n f r : 2 <= r -> (forall i j, i < j <= n -> f i < f j) -> ∑ (S n) (fun i => power (f i) r) < power (S (f n)) r.
proof: Proof. intros Hr. revert f. induction n as [ | n IHn ]; intros f Hf. + rewrite msum_1; auto; apply power_smono_l; auto. + rewrite msum_plus1; auto. rewrite power_S. apply Nat.lt_le_trans with (power (S (f n)) r + power (f (S n)) r). * apply Nat.add_lt_mono_r; auto. apply IHn; intros; apply Hf; lia. * assert (power (S (f n)) r <= power (f (S n)) r) as H. { apply power_mono_l; try lia; apply Hf; lia. } apply Nat.le_trans with (2 * power (f (S n)) r); try lia. apply Nat.mul_le_mono; auto. Qed.
imports: Arith Lia List Bool Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd sums rel_iter bool_nat power_decomp prime)