proposition: Lemma can_to_cat x a l1 l2 : x \in l1 -> C[x]_(a, l1 ++ l2) = C[x]_(a, l1).
proof: Proof. move=> xIl1. rewrite /can_to find_cat; case: (boolP (has _ _)). by rewrite nth_cat has_find => ->. by move/hasPn/(_ x xIl1); rewrite symconnect0. Qed.
imports: mathcomp(all_ssreflect) extra