proposition: Theorem sum_sum_regroup : { g | ∑ n (fun i => ∑ i (fun j => power (f i + f j) r)) = ∑ (2*k) (fun i => g i * power i r) /\ forall i, g i <= n }.
proof: Proof. Proof using Hf1 Hf2. revert n f Hf1 Hf2. induction n as [ | p IHp ]; intros f Hf1 Hf2. + exists (fun _ => 0); split; auto. rewrite msum_0. simpl; rewrite msum_of_unit; auto. + destruct (IHp f) as (g & H1 & H2). * intros; apply Hf1; lia. * intros; apply Hf2; lia. * destruct sum_regroup with (r := r) (n := p) (f := fun j => f p + f j) (k := 2*k) as (g1 & G1 & G2 & G3). - intros i Hi; generalize (@Hf1 p) (@Hf2 i p); intros; lia. - intros i j H; generalize (@Hf2 i j); intros; lia. - assert (forall i, g1 i <= 1) as G4. { intro i; destruct (le_lt_dec (2*k) i); auto; rewrite G3; lia. } exists (fun i => g i + g1 i); split. ++ rewrite msum_plus1; auto. rewrite H1, G1, <- msum_sum; auto. 2: intros; ring. apply msum_ext; intros; ring. ++ intros i. generalize (H2 i) (G4 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)