proposition: Lemma symconnect_can_to x a l : x \in l -> C[x]_(a, l) =[a]= x.
proof: Proof. move=> xIl; rewrite symconnect_sym; apply: nth_find. by apply/hasP; exists x => //; exact: symconnect0. Qed.
imports: mathcomp(all_ssreflect) extra