proposition: Lemma graph_rel_known_port x y : graph_rel x y -> (known_port x.1 /\ known_port y.1) /\ (x.1 != y.1 /\ y.2 = negb x.2).
proof: Proof. case: x y => [[x|x][|]] [[y|y][|]] //=. - move/andP => [Hdom Hed]. move: (Hdom). rewrite inE => /andP [_] ->. move/setP/(_ y): (edom_codom c). rewrite -(eqP Hed) imset_f // inE. by move/esym/andP => [_] ->. - move/existsP => [s] /and4P[Hsg Hos Ho0s Hoo0]. by split; split => //; apply/bigcupP; exists s. - move/andP => [Hdom Hed]. move: (Hdom). rewrite inE => /andP [_] ->. move/setP/(_ x): (edom_codom c). rewrite -(eqP Hed) imset_f // inE. by move/esym/andP => [_] ->. - move/existsP => [s] /and4P[Hsg Hos Ho0s Hoo0]. by split; split => //; apply/bigcupP; exists s. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist subgraph_partition tanner