proposition: Lemma add_edge_connected (G : sgraph) (i o : G) (U : {set G}) : @connected G U -> @connected (add_edge i o) U.
proof: Proof. move => con1 x y xU yU. apply: connect_mono (con1 _ _ xU yU) => {x y xU yU} x y. by rewrite {2}/edge_rel /= -andbA => /and3P[-> -> ->]. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph)