proposition: Fact power_divides_sum_power r p n f : 2 <= r -> 0 < n -> (forall i j, i < j < n -> f i < f j) -> divides (power p r) (∑ n (fun i => power (f i) r)) <-> p <= f 0.
proof: Proof. intros Hr Hn Hf. split. + destruct inc_seq_split_lt with (k := p) (1 := Hf) as (k & H1 & H2 & H3). replace n with (k+(n-k)) by lia. rewrite msum_plus; auto. rewrite Nat.add_comm; intros H. apply divides_plus_inv in H. 2: apply divides_msum; intros; apply divides_power, H3; lia. destruct k as [ | k ]. * apply H3; lia. * apply divides_lt in H. - rewrite msum_S in H. generalize (@power_ge_1 (f 0) r); intros; lia. - apply sum_powers_inc_lt; auto. intros; apply Hf; lia. + intros H. apply divides_msum. intros i Hi; apply divides_power. apply Nat.le_trans with (1 := H). destruct i; auto. generalize (Hf 0 (S i)); intros; lia. Qed.
imports: Arith Lia List Bool Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd sums rel_iter bool_nat power_decomp prime)