proposition: Fact rel_iter_plus n m x y : rel_iter (n+m) x y <-> exists a, rel_iter n x a /\ rel_iter m a y.
proof: Proof. revert x y; induction n as [ | n IHn ]; intros x y; simpl. + split. * exists x; split; auto. * intros (? & ? & ?); subst; auto. + split. * intros (a & H1 & H2). apply IHn in H2. destruct H2 as (b & H2 & H3). exists b; split; auto; exists a; auto. * intros (a & (b & H1 & H2) & H3). exists b; split; auto. apply IHn; exists a; auto. Qed.
imports: Arith Nat Lia Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd prime binomial sums)