proposition: Lemma rev_path_rcons a b p : symmetric g -> path g a (rcons p b) = path g b (rcons (rev p) a).
proof: Proof. move=> HR. elim: p a b => [|c p Hp] a b /=. by rewrite HR. rewrite rev_cons -(cats1 _ a) cat_path -Hp /= last_rcons /=. by rewrite (HR a) andbC andbT. Qed.
imports: mathcomp(all_ssreflect fingroup perm)