proposition: Lemma rtc_trans : transitive rtc.
proof: Proof. rewrite /rtc=>x y z; case: decP=>// Dy; case: decP=>// Dx. by case: decP=>// Dz; apply: connect_trans. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq choice fintype path fingraph) pcm(options axioms pred prelude finmap seqext)