proposition: Lemma clos_rt_rtn1_iff : forall x y, clos_refl_trans R x y <-> clos_refl_trans_n1 R x y.
proof: Proof. split. - apply clos_rt_rtn1. - apply clos_rtn1_rt. Defined.
imports: CRelationClasses Equations.Init Equations.Type.Logic Equations.Type.Relation