proposition: Lemma clinkC : connect_sym clink.
proof: Proof. by apply: relU_sym; [apply: (fconnect_sym (finv_inj nodeI)) | apply: cfaceC]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) mathcomp(choice fintype path fingraph)