proposition: Lemma clinkP x y : reflect (x = node y \/ face x = y) (clink x y).
proof: Proof. by rewrite /clink /= (canF_eq (f_finv nodeI)); apply: pred2P. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) mathcomp(choice fintype path fingraph)