proposition: Lemma trans_clos_left_aux : forall X (T : X -> X -> Prop) z y z0, T z y -> clos_refl_trans X T z0 z -> clos_trans_1n X T z0 y.
proof: Proof. intros X T z y z0 H Hrt. remember (@Relation_Operators.t1n_step X T z y H) as G. clear HeqG; clear H. remember (@clos_rt_rt1n _ T z0 z Hrt) as F. clear HeqF. clear Hrt. induction F. apply G. econstructor 2. apply H. apply IHF. apply G. Qed.
imports: Coq(Arith Relations)