proposition: Lemma clos_trans_t1n : forall x y, clos_trans R x y -> clos_trans_1n R x y.
proof: Proof. induction 1 as [x y H|x y z H IHclos_trans1 H0 IHclos_trans2]. - left; assumption. - generalize IHclos_trans2; clear IHclos_trans2. induction IHclos_trans1 as [x y H1|x y z0 H1 ? IHIHclos_trans1]. + right with y; auto. + right with y; auto. eapply IHIHclos_trans1; auto. apply clos_t1n_trans; auto. Qed.
imports: Relation_Definitions Relation_Operators