proposition: Theorem RstarRplus_RRstar : forall (U:Type) (R:Relation U) (x y z:U), Rstar U R x y -> Rplus U R y z -> exists u : _, R x u /\ Rstar U 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 x1 y0 H'1; exists y0; auto with sets. + intros x1 y0 z0 H'1 H'2 H'3; exists y0; auto with sets. - intros x0 y0 z0 H'0 H'1 H'2 H'3; exists y0. split; [ try assumption | idtac ]. apply T1 with z0; auto with sets. Qed.
imports: Relations_1 Relations_1_facts Relations_2