proposition: Lemma clos_tn1_trans : forall x y, clos_trans_n1 R x y -> clos_trans R x y.
proof: Proof. induction 1 as [y H|y z H H0 ?]. - left; assumption. - right with y; auto. left; assumption. Qed.
imports: Relation_Definitions Relation_Operators