proposition: Lemma clos_trans_tn1 : forall x y, clos_trans R x y -> clos_trans_n1 R x y.
proof: Proof. induction 1 as [x y H|x y z H IHclos_trans1 H0 IHclos_trans2]. - left; assumption. - elim IHclos_trans2. + intro y0; right with y. * auto. * auto. + intro y0; intros. right with y0; auto. Qed.
imports: Relation_Definitions Relation_Operators