proposition: Lemma rt1n_ind_right : forall (P : A -> Type) (z:A), P z -> (forall x y, R x y -> clos_refl_trans_1n R y z -> P y -> P x) -> forall x, clos_refl_trans_1n R x z -> P x.
proof: Proof. induction 3; auto. apply X0 with y; auto. Defined.
imports: CRelationClasses Equations.Init Equations.Type.Logic Equations.Type.Relation