fact: Definition rtc (x y : nat) : bool := if decP (@idP (x \in h)) is left pfx then if decP (@idP (y \in h)) is left pfy then connect Rtp (Sub x pfx) (Sub y pfy) else false else false.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq choice fintype path fingraph) pcm(options axioms pred prelude finmap seqext)