proposition: Lemma refl_trans_clos_R : forall x y z, refl_trans_clos R x y -> R y z -> refl_trans_clos R x z.
proof: Proof. intros x y z Rs_x_y R_y_z. apply refl_trans_clos_is_trans with y. assumption. do 2 constructor;assumption. Qed.
imports: CoLoR(closure) Coq(Relation_Operators)