proposition: Remark gcomp_dual : (gcomp : rel dual) =2 (gcomp : rel G).
proof: Proof. by move=> x y; rewrite -!clink_glink (eq_connect clink_dual). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) mathcomp(choice fintype path fingraph)