proposition: Lemma trivial_connector A B : exists p : 'I_#|A :&: B| -> pathS G, connector A B p.
proof: Proof. exists (fun i => PathS (idp (enum_val i))). split. - move => i /=. exact: irred_idp. - move => i /=. case/setIP : (enum_valP i) => iA iB. apply/setP => z. rewrite !inE /= mem_idp. case e: (_ == _) => //. by rewrite (eqP e). - move => i /=. case/setIP : (enum_valP i) => iA iB. apply/setP => z. rewrite !inE /= mem_idp. case e: (_ == _) => //. by rewrite (eqP e). - move => i j. apply: contraNeq => /set0Pn [x /setIP[]]. by rewrite !inE /= !mem_idp => /eqP-> /eqP /enum_val_inj->. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph mgraph sgraph set_tac)