proposition: Lemma add_edge_keep_connected_l (G : sgraph) s1 s2 A: @connected (@add_edge G s1 s2) A -> s1 \notin A -> @connected G A.
proof: Proof. move => H s1A x y xA yA. case: (altP (x =P y)) => [-> //|xDy]. case/connect_irredRP : (H _ _ xA yA) => // p Ip subA. case: (add_edge_avoid p) => [|q Hq]; first by rewrite notinD. apply connectRI with q. move => u. rewrite mem_path Hq -(mem_path p). by set_tac. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph) GraphTheory(set_tac)