proposition: Lemma clos_rst_rstn1_iff : forall x y, clos_refl_sym_trans R x y <-> clos_refl_sym_trans_n1 R x y.
proof: Proof. split. - apply clos_rst_rstn1. - apply clos_rstn1_rst. Qed.
imports: Relation_Definitions Relation_Operators