proposition: Lemma eq_path_in (P : pred T) a q : {in P &, g =2 g'} -> all P (a :: q) -> path g a q = path g' a q.
proof: Proof. move=> Heq. elim: q a => [|b q] //= IH a /andP [HPa HPb]. rewrite IH // Heq //. by move/andP: HPb => []. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist