proposition: Lemma gcomp_mirror : (gcomp : rel mirror) =2 (gcomp : rel G).
proof: Proof. move=> x y; rewrite -!clink_glink. by rewrite (eq_connect clink_mirror) (same_connect_rev clinkC). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) mathcomp(choice fintype path fingraph)