proposition: Theorem RstarRplus_RRstar : forall (U : Type) (R : Relation U) (x y z : U), Rstar R x y -> Rplus R y z -> exists u : U, R x u /\ Rstar R u z.
proof: Proof. generalize Rstar_contains_Rplus; intro T; red in T. generalize Rstar_transitive; intro T1; red in T1. intros U R x y z H'; elim H'. intros x0 H'0; elim H'0. intros; exists y0; auto. intros; exists y0; auto. intros; exists y0; auto. split; [ try assumption | idtac ]. apply T1 with z0; auto. Qed.
imports: Relations Confluence