proposition: Fact sum_powers_euclid r n f e : (forall j, j < n -> e 1 <= e (S j)) -> sum_powers r (S n) f e = f 0 * power (e 0) r + sum_powers r n (fun i => f (S i)) (fun i => e (S i) - e 1) * power (e 1) r.
proof: Proof. intros Hf; simpl; 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 _ Hi); lia. Qed.
imports: Arith Nat Lia List Bool Setoid Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list utils_nat bool_list gcd sums power_decomp)