proposition: Lemma rtc_tc x y : tc x y -> rtc x y.
proof: Proof. case/andP=>Dx /hasP [z Dz] /andP [Rxz]. by apply: rtc_trans (rtc1 Dx Dz Rxz). Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq choice fintype path fingraph) pcm(options axioms pred prelude finmap seqext)