proposition: Lemma eq_can_to x a b l : a =1 b -> C[x]_(a, l) = C[x]_(b, l).
proof: Proof. move=> aEb; rewrite /can_to /=. congr (nth _ _ _). apply: eq_find => y. by apply: eq_symconnect_to. Qed.
imports: mathcomp(all_ssreflect) extra