proposition: Lemma trans_clos_left : forall X (T : X -> X -> Prop) z y z0, T z y -> clos_refl_trans X T z0 z -> clos_refl_trans X T z0 y.
proof: Proof. intros. eapply rt_trans. apply H0. apply rt_step. apply H. Qed.
imports: Coq(Arith Relations)