proposition: Lemma rel_iter_iter_bound n x y : rel_iter R n x y -> rel_iter_bound n x y.
proof: Proof. Proof using Hk1. intros H. apply rel_iter_sequence in H. destruct H as (f & H1 & H2 & H3). assert (forall i, i <= n -> f i <= power i (S k) * x) as Hf. { induction i as [ | i IHi ]; intros Hi; simpl; try lia. specialize (H3 _ Hi). apply Hk' in H3. apply Nat.le_trans with (1 := H3). rewrite power_S, <- Nat.mul_assoc. apply Nat.mul_le_mono; auto. apply IHi; lia. } set (q := S (x * power n (S k))). assert (q <> 0) as Hq by discriminate. assert (forall i, i <= n -> f i < q) as Hfq. { unfold q; intros i Hi. apply le_n_S, Nat.le_trans with (1 := Hf _ Hi). rewrite Nat.mul_comm; apply Nat.mul_le_mono; auto. apply power_mono; auto; lia. } set (c := ∑ (S n) (fun i => f i * power i q)). assert (forall i, i <= n -> is_digit c q i (f i)) as Hc. { intros i Hi; split; auto. + exists (∑ (n-i) (fun j => f (1+i+j) * power j q)), (∑ i (fun i => f i * power i q)); split. 2: apply sum_power_lt; auto; intros; apply Hfq; lia. unfold c; replace (S n) with (i+S (n - i)) by lia. rewrite msum_plus, Nat.add_comm; f_equal; auto. rewrite msum_ext with (g := fun k => power i q*(f (i+k)*power k q)). * rewrite sum_0n_scal_l, Nat.mul_comm; f_equal. rewrite msum_S, Nat.add_comm; f_equal. 2: simpl; rewrite Nat.mul_1_r; f_equal; lia. rewrite (Nat.mul_comm _ q), <- sum_0n_scal_l. apply msum_ext. intros j _. replace (i+S j) with (1+i+j) by lia. rewrite power_S; ring. * intros j _; rewrite power_plus; ring. } exists q, c; split; [ | split; [ | split ] ]. + unfold q; auto. + intros i Hi; exists (f i), (f (S i)). split; [ | split ]. * apply Hc; lia. * apply Hc; lia. * apply H3; auto. + rewrite <- H1; apply Hc; lia. + rewrite <- H2; apply Hc; lia. Qed.
imports: Arith Nat Lia Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd prime binomial sums)