proposition: Lemma clos_rst1n_rst : forall x y, clos_refl_sym_trans_1n R x y -> clos_refl_sym_trans R x y.
proof: Proof. induction 1 as [|x y z H]. - constructor 2. - constructor 4 with y; auto. case H;[constructor 1|constructor 3; constructor 1]; auto. Qed.
imports: Relation_Definitions Relation_Operators