proposition: Lemma clos_rt1n_rt : forall x y, clos_refl_trans_1n R x y -> clos_refl_trans R x y.
proof: Proof. induction 1 as [|x y z]. - constructor 2. - constructor 3 with y; auto. constructor 1; auto. Qed.
imports: Relation_Definitions Relation_Operators