proposition: Lemma clos_rt_rtn1 : forall x y, clos_refl_trans R x y -> clos_refl_trans_n1 R x y.
proof: Proof. induction 1 as [| |x y z H1 IH1 H2 IH2]. - apply clos_rtn1_step; auto. - left. - elim IH2; auto. intro y0; intros. right with y0; auto. Qed.
imports: Relation_Definitions Relation_Operators