proposition: Theorem Rstar_transitive : forall (U:Type) (R:Relation U), Transitive U (Rstar U R).
proof: Proof. intros U R; red. intros x y z H'; elim H'; auto with sets. intros x0 y0 z0 H'0 H'1 H'2 H'3; apply Rstar_n with y0; auto with sets. Qed.
imports: Relations_1 Relations_1_facts Relations_2