proposition: Lemma clos_refl_trans_right {R : X -> X -> Prop} x y z : R y z -> clos_refl_trans _ R x y -> clos_trans_n1 _ R x z.
proof: Proof. intros Ryz Rxy. apply clos_rt_rtn1_iff in Rxy. induction Rxy in Ryz, z |- *. econstructor 1; eauto. econstructor 2; eauto. Defined.
imports: Equations(Equations) Examples.Fin Relations Utf8 Relations Wellfounded Setoid RelationClasses Morphisms Lia Bool List Arith String Coq(FunctionalExtensionality)