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. intros Hf Ha Hb E i Hi. generalize (power_decomp_is_digit _ _ Hf Ha Hi) (power_decomp_is_digit _ _ Hf Hb Hi). rewrite E; apply is_digit_fun. Qed.
imports: Arith Nat Lia Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd rel_iter sums)