proposition: Remark clink_dual : @clink dual =2 @clink G.
proof: Proof. by move=> x y; rewrite /clink /= (finv_inv faceI) orbC. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) mathcomp(choice fintype path fingraph)