proposition: Fact rel_iter_1 x y : rel_iter 1 x y <-> R x y.
proof: Proof. simpl; split. * intros (? & ? & ?); subst; auto. * exists y; auto. Qed.
imports: Arith Nat Lia Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd prime binomial sums)