proposition: Lemma sjoin_disconnected (G H : sgraph) (x : G) (y : H) : ~~ connect (--) (inl x : (G ∔ H)%sg) (inr y).
proof: Proof. apply: contraTN isT => /connectP [p]; elim: p x => // -[/=|//] z p IHp x. case/andP => _ . exact: IHp. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph)