proposition: Lemma rtcT (h : seq nat) (R : rel nat) x y : (forall x y, R x y -> (x \in h) && (y \in h)) -> transitive R -> rtc h R x y -> R x y || (x == y) && (x \in h).
proof: Proof. move=>Rcond Tr /rtcP [|Dx [n]]; first by move=>?? /Rcond/andP [->->]. elim: n x Dx=>[|n IH] x Dx /=; first by move=><-; rewrite eq_refl Dx orbT. case=>z [Rxz]; case/Rcond/andP: (Rxz)=>-> Dz /(IH _ Dz). by case: eqP Rxz=>[<- ->//|_ Rxz]; rewrite orbF=>/(Tr _ _ _ Rxz)=>->. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq choice fintype path fingraph) pcm(options axioms pred prelude finmap seqext)