proposition: Lemma cpo_antisym : {in cp i o&,antisymmetric cpo}.
proof: Proof. Proof using. move => x y /cpP/(_ the_uPath) Hx _. rewrite /cpo -eqn_leq =>/eqP. exact: idx_inj. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph) GraphTheory(sgraph connectivity)