proposition: Fact sum_powers_injective r n f m g : 2 <= r -> (forall i j, i < j < n -> f i < f j) -> (forall i j, i < j < m -> g i < g j) -> ∑ n (fun i => power (f i) r) = ∑ m (fun i => power (g i) r) -> n = m /\ forall i, i < n -> f i = g i.
proof: Proof. intros Hr; revert m f g. induction n as [ | n IHn ]; intros m f g Hf Hg. + rewrite msum_0. destruct m as [ | m ]. * rewrite msum_0; split; auto; intros; lia. * rewrite msum_S. generalize (@power_ge_1 (g 0) r); intros; exfalso; lia. + destruct m as [ | m ]. * rewrite msum_0, msum_S; intros; exfalso. generalize (@power_ge_1 (f 0) r); intros; exfalso; lia. * destruct (lt_eq_lt_dec (f n) (g m)) as [ [E|E]| E]. - rewrite msum_plus1 with (n := m); auto. intros; exfalso. assert (∑ (S n) (fun i => power (f i) r) < power (g m) r) as C; try lia. apply sum_powers_inc_lt; auto. intros i Hi. destruct (eq_nat_dec i n); subst; auto. apply Nat.lt_trans with (2 := E), Hf; lia. - do 2 (rewrite msum_plus1; auto); intros C. destruct (IHn m f g) as (H1 & H2). ++ intros; apply Hf; lia. ++ intros; apply Hg; lia. ++ rewrite E in C; lia. ++ split; subst; auto. intros i Hi. destruct (eq_nat_dec i m); subst; auto. apply H2; lia. - rewrite msum_plus1 with (n := n); auto. intros; exfalso. assert (∑ (S m) (fun i => power (g i) r) < power (f n) r) as C; try lia. apply sum_powers_inc_lt; auto. intros i Hi. destruct (eq_nat_dec i m); subst; auto. apply Nat.lt_trans with (2 := E), Hg; lia. Qed.
imports: Arith Lia List Bool Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd sums rel_iter bool_nat power_decomp prime)