proposition: Lemma flip_seq_path x p : path graph_rel x p -> path graph_rel (last (flip x) (map flip p)) (map flip (rev (belast x p))).
proof: Proof. elim: p x => // a l IH [x b] /andP [Hp1 Hp2]. rewrite rev_cons map_rcons rcons_path {7}/flip /= IH //=. destruct l as [|[a' b'] l]. simpl map. destruct a; simpl last. by rewrite -/(flip (x, b)) flip_graph_rel. rewrite rev_cons map_rcons last_rcons. by rewrite -/(flip (x, b)) flip_graph_rel. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist subgraph_partition tanner