proposition: Theorem power_decomp_unique' n f a b : (forall i j, i < j < n -> f i < f j) -> (forall i, i < n -> a i < p) -> (forall i, i < n -> b i < p) -> ∑ n (fun i => a i * power (f i) p) = ∑ n (fun i => b i * power (f i) p) -> forall i, i < n -> a i = b i.
proof: Proof. Proof using Hp. revert f a b. induction n as [ | n IHn ]; intros f a b Hf Ha Hb. + intros; lia. + assert (forall i, 0 < i < S n -> f 0 < f i) by (intros; apply Hf; lia). do 2 (rewrite power_decomp_factor; auto). intros E. apply div_rem_uniq in E; auto. * destruct E as (E1 & E2). intros [ | i ] Hi. - revert E2; rewrite Nat.mul_cancel_r; auto. - apply IHn with (4 := E1); try lia. ++ intros u j Hu; apply lt_minus_cancel; split; apply Hf; lia. ++ intros; apply Ha; lia. ++ intros; apply Hb; lia. * rewrite power_S. apply Nat.mul_lt_mono_pos_r. - apply power_ge_1; lia. - apply Ha; lia. * rewrite power_S. apply Nat.mul_lt_mono_pos_r. - apply power_ge_1; lia. - apply Hb; lia. Qed.
imports: Arith Nat Lia Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd rel_iter sums)