proposition: Fact rel_iter_S n x y : rel_iter (S n) x y <-> exists a, rel_iter n x a /\ R a y.
proof: Proof. replace (S n) with (n+1) by lia. rewrite rel_iter_plus. split; intros (a & H1 & H2); exists a; revert H1 H2; rewrite rel_iter_1; auto. Qed.
imports: Arith Nat Lia Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd prime binomial sums)