proposition: Lemma tseq_rel_connect_before (g : rel V) x y : acyclic g -> connect g x y -> before (tseq (rgraph g)) x y.
proof: Proof. move=> acycg cgxy; have rgK := rgraphK g. by apply: tseq_connect_before; rewrite (eq_acyclic rgK, eq_connect rgK). Qed.
imports: mathcomp(all_ssreflect) extra acyclic kosaraju