proposition: Lemma setF_pr2 A a b: inc A setF -> inc a A -> chain_related R a b -> inc b A.
proof: Proof. move=> As aA [c [cc hcx <-]]. rewrite - hcx in aA; clear hcx. elim: c cc aA. move=> u v /= Ruv uA; apply: (setF_pr As uA Ruv). move=> u c h /= [uh cc] uA. apply: h=>//;apply: (setF_pr As uA uh). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)