proposition: Lemma glinkC : connect_sym glink.
proof: Proof. by do !apply: relU_sym; [apply: cedgeC | apply: cnodeC | apply: cfaceC]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) mathcomp(choice fintype path fingraph)