proposition: Lemma flip_graph_rel x y : graph_rel x y -> graph_rel (flip y) (flip x).
proof: Proof. case: x y => [[x|x][|]] [[y|y][|]] //=. - move/existsP => [s /and4P[Ha Hb Hc Hd]]. apply/existsP; exists s. by rewrite Ha Hb Hc eq_sym. - move/existsP => [s /and4P[Ha Hb Hc Hd]]. apply/existsP; exists s. by rewrite Ha Hb Hc eq_sym. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist subgraph_partition tanner