proposition: Lemma tcT (h : seq nat) (R : rel nat) : (forall x y, R x y -> (x \in h) && (y \in h)) -> transitive R -> tc h R =2 R.
proof: Proof. move=>Rcond Tr x y; apply/idP/idP; last first. - by move=>H; case/andP: (Rcond _ _ H)=>Dx Dy; apply: tc1. case/andP=>Dx /hasP [z Dz] /andP [Rxz] /(rtcT Rcond Tr). by case: eqP=>[<-|_] //; rewrite orbF; apply: Tr Rxz. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq choice fintype path fingraph) pcm(options axioms pred prelude finmap seqext)