proposition: Lemma rel_iter_seq_iter n x y : rel_iter_seq n x y -> rel_iter R n x y.
proof: Proof. revert y; induction n as [ | n IHn ]; intros y. * intros (q & c & H2 & H3 & H4). red in H2. simpl; revert H3 H4; apply is_digit_fun. * rewrite rel_iter_S. intros (q & c & H2 & H3 & H4). red in H2. assert (0 < q) as Hq. { destruct H3; lia. } assert (exists z, is_digit c q n z) as H6. { exists (rem (div c (power n q)) q). split. + apply div_rem_spec2; lia. + exists (div (div c (power n q)) q), (rem c (power n q)); split. 2: apply div_rem_spec2; red; rewrite power_0_inv; lia. rewrite <- div_rem_spec1 with (p := q). apply div_rem_spec1. } destruct H6 as (z & H6); exists z; split. + apply IHn. exists q, c; msplit 2; auto. intros i Hi; apply H2; lia. + destruct (H2 n) as (u & v & G1 & G2 & G3); auto. rewrite is_digit_fun with (1 := H4) (2 := G2), is_digit_fun with (1 := H6) (2 := G1); auto. Qed.
imports: Arith Nat Lia Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd prime binomial sums)