proposition: Lemma join_disc (x : G1) (y : G2) : connect join_rel (inl x) (inr y) = false.
proof: Proof. apply/negP. case/connectP => p. elim: p x => // [[a|a]] //= p IH x. case/andP => _. exact: IH. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph)