proposition: Lemma connect_idemp (T : finType) (R : rel T) : reflexive R -> transitive R -> connect R =2 R.
proof: Proof. move=>Rr Tr x y; apply/connectP; case: ifP=>[Rxy|H [p P Ly]]. - by exists [:: y]=>//=; rewrite Rxy. by move: (path_lastR Rr Tr P); rewrite -Ly H. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq choice fintype path fingraph) pcm(options axioms pred prelude finmap seqext)