proposition: Lemma clos_rt_rt1n : forall x y, clos_refl_trans R x y -> clos_refl_trans_1n R x y.
proof: Proof. induction 1 as [| |x y z H IHclos_refl_trans1 H0 IHclos_refl_trans2]. - apply clos_rt1n_step; assumption. - left. - generalize IHclos_refl_trans2; clear IHclos_refl_trans2; induction IHclos_refl_trans1 as [|x y z0 H1 ? IH]; auto. right with y; auto. eapply IH; auto. apply clos_rt1n_rt; auto. Qed.
imports: Relation_Definitions Relation_Operators