proposition: Lemma power_decomp_is_digit n a f : (forall i j, i < j < n -> f i < f j) -> (forall i, i < n -> a i < p) -> forall i, i < n -> is_digit (∑ n (fun i => a i * power (f i) p)) p (f i) (a i).
proof: Proof. Proof using Hp. intros Hf Ha. induction n as [ | n IHn ]; intros i Hi. + lia. + split; auto. exists (∑ (n-i) (fun j => a (S i + j) * power (f (S i+j) - f i - 1) p)), (∑ i (fun j => a j * power (f j) p)); split. - replace (S n) with (S i + (n-i)) by lia. rewrite msum_plus, msum_plus1; auto. rewrite <- Nat.add_assoc, Nat.add_comm; f_equal. rewrite Nat.mul_add_distr_r, Nat.add_comm; f_equal. rewrite <- Nat.mul_assoc, Nat.mul_comm, <- sum_0n_scal_l. apply msum_ext. intros j Hj. rewrite (Nat.mul_comm (_ * _)); repeat rewrite <- Nat.mul_assoc; f_equal. rewrite <- power_S, <- power_plus; f_equal. generalize (Hf i (S i+j)); intros; lia. - apply power_decomp_lt; auto. * intros; apply Hf; lia. * intros; apply Ha; lia. Qed.
imports: Arith Nat Lia Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd rel_iter sums)