proposition: Lemma before_can_to x y a l : x \in l -> y \in l -> x =[a]= y -> C[x]_(a, l) =[l]< y.
proof: Proof. move=> Hx Hy; rewrite symconnect_sym => Hr. have F : has (symconnect (relto a r) x) l. by apply/hasP; exists y => //; rewrite symconnect_sym. rewrite /before /can_to index_find //. case: leqP => // /(before_find x). by rewrite nth_index // symconnect_sym Hr. Qed.
imports: mathcomp(all_ssreflect) extra