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