proposition: Fact sum_powers_inc_lt n f p r : 2 <= r -> (forall i, i < n -> f i < p) -> (forall i j, i < j < n -> f i < f j) -> ∑ n (fun i => power (f i) r) < power p r.
proof: Proof. destruct n as [ | n ]. + intros H _ _; rewrite msum_0; apply power_ge_1; lia. + intros H1 H2 H3. apply Nat.lt_le_trans with (power (S (f n)) r). * apply sum_powers_inc_lt_last; auto. intros; apply H3; lia. * apply power_mono_l; try lia. apply H2; auto. Qed.
imports: Arith Lia List Bool Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd sums rel_iter bool_nat power_decomp prime)