proposition: Fact sum_regroup r k n f : (forall i, i < n -> f i < k) -> (forall i j, i < j < n -> f i < f j) -> { g | ∑ n (fun i => power (f i) r) = ∑ k (fun i => g i * power i r) /\ (forall i, i < k -> g i <= 1) /\ (forall i, k <= i -> g i = 0) }.
proof: Proof. revert k f; induction n as [ | n IHn ]; intros k f Hf1 Hf2. + exists (fun _ => 0); split; auto. rewrite msum_0, msum_of_unit; auto. + destruct (IHn (f n) f) as (g & H1 & H2 & H3). * intros; apply Hf2; lia. * intros; apply Hf2; lia. * exists (fun i => if eq_nat_dec i (f n) then 1 else g i). split; [ | split ]. - rewrite msum_plus1, H1; auto. replace k with (f n + S (k - f n -1)). 2: generalize (Hf1 n); intros; lia. rewrite msum_plus; auto; f_equal. ++ apply msum_ext. intros i He. destruct (eq_nat_dec i (f n)); try ring; lia. ++ rewrite msum_S, msum_of_unit; auto. ** repeat (rewrite Nat.add_comm; simpl). destruct (eq_nat_dec (f n) (f n)); try ring; lia. ** intros i Hi. destruct (eq_nat_dec (f n+S i) (f n)); try lia. rewrite H3; lia. - intros i Hi. destruct (eq_nat_dec i (f n)); auto. destruct (le_lt_dec (f n) i). ++ rewrite H3; lia. ++ apply H2; lia. - intros i Hi. generalize (Hf1 n); intros. destruct (eq_nat_dec i (f n)); try lia. apply H3; lia. Qed.
imports: Arith Lia List Bool Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd sums rel_iter bool_nat power_decomp prime)