proposition: Lemma clos_refl_trans_ind_right : forall (P : A -> Prop) (z:A), P z -> (forall x y, R x y -> P y -> clos_refl_trans R y z -> P x) -> forall x, clos_refl_trans R x z -> P x.
proof: Proof. intros P z Hz IH x Hxz. apply clos_rt_rt1n_iff in Hxz. elim Hxz using rt1n_ind_right; auto. clear x Hxz. intros x y Hxy Hyz Hy. apply clos_rt_rt1n_iff in Hyz. eauto. Qed.
imports: Relation_Definitions Relation_Operators