proposition: Fact rel_iter_sequence n x y : rel_iter n x y <-> exists f, f 0 = x /\ f n = y /\ forall i, i < n -> R (f i) (f (S i)).
proof: Proof. split. * revert x y; induction n as [ | n IHn ]; simpl; intros x y. + intros; subst y; exists (fun _ => x); repeat split; auto; intros; lia. + intros (a & H1 & H2). destruct IHn with (1 := H2) as (f & H3 & H4 & H5). exists (fun i => match i with 0 => x | S i => f i end); repeat split; auto. intros [ | i ] Hi; subst; auto. apply H5; lia. * intros (f & H1 & H2 & H3); subst x y. induction n as [ | n IHn ]. + simpl; auto. + rewrite rel_iter_S. exists (f n); split; auto. Qed.
imports: Arith Nat Lia Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd prime binomial sums)