proposition: Lemma cons_uniq_path a b s : g a b -> a \notin b :: s -> uniq_path b s -> uniq_path a (b :: s).
proof: Proof. move=> Hab Has /andP /= [Hpi Hun]. rewrite /uniq_path /=. by rewrite Hun Hpi Hab Has. Qed.
imports: mathcomp(all_ssreflect fingroup perm)