proposition: Lemma gpath_rev t1 t2 p : gpath r t1 t2 p -> gpath (fun z : T => r^~ z) t2 t1 (rev (belast t1 p)).
proof: Proof. move=> /gpathP[H1 H2] H3. apply/gpathP; split => //. - by rewrite -rev_path H2 in H1. - case: (p) H2 => //= a p1. by rewrite /= rev_cons last_rcons. by rewrite size_rev size_belast -gdist_sym. Qed.
imports: mathcomp(all_ssreflect)