proposition: Theorem power_decomp_factor n f a : (forall i, 0 < i < S n -> f 0 < f i) -> ∑ (S n) (fun i => a i * power (f i) p) = ∑ n (fun i => a (S i) * power (f (S i) - f 0 - 1) p) * power (S (f 0)) p + a 0 * power (f 0) p.
proof: Proof. Proof using Hp. intros Hf. rewrite msum_S, Nat.add_comm; f_equal. rewrite <- sum_0n_scal_r. apply msum_ext. intros i Hi. rewrite <- Nat.mul_assoc; f_equal. rewrite <- power_plus; f_equal. generalize (Hf (S i)); intros; lia. Qed.
imports: Arith Nat Lia Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd rel_iter sums)