proposition: Remark gcomp_permN : (gcomp : rel permN) =2 (gcomp : rel G).
proof: Proof. by apply: eq_connect => x y; rewrite /glink /= orbA orbC. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) mathcomp(choice fintype path fingraph)