proposition: Lemma before_can_toW x a b l : x \in l -> b \subset a -> C[x]_(a, l) =[l]< C[x]_(b, l).
proof: Proof. move=> xIl Hs. have Hs1 : has (symconnect (relto a r) x) l. by apply/hasP; exists x => //; exact: symconnect0. have Hs2 : has (symconnect (relto b r) x) l. by apply/hasP; exists x => //; exact: symconnect0. rewrite /before /can_to !index_find //. apply: sub_find => z. by apply: sub_symconnect_to. Qed.
imports: mathcomp(all_ssreflect) extra