proposition: Lemma rt1n_ind_right : forall (P : A -> Prop) (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. intros P z H H0 x; induction 1 as [|x y z]; auto. apply H0 with y; auto. Qed.
imports: Relation_Definitions Relation_Operators