proposition: Remark clink_mirror : @clink mirror =2 (fun x y : G => clink y x).
proof: Proof. move=> x y; rewrite !(sameP clinkP pred2P) -(eq_sym y) eq_sym /=. by rewrite (canF_eq (f_finv nodeI)) -(canF_eq (finv_f faceI)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) mathcomp(choice fintype path fingraph)