proposition: Lemma eq_tsorted a b l : a =1 b -> TS[a, l] -> TS[b , l].
proof: Proof. move=> aEb [/= lSa Ca Ba]. have aE2b : relto a r =2 relto b r by move=> x y; rewrite /= -topredE /= aEb. split => /= [|x y xIl xCy|x y xIl xCy]. - apply: subset_trans lSa _. by apply/subsetP=> i; rewrite -!topredE /= aEb. - by apply: Ca xIl _; rewrite (eq_connect aE2b). rewrite -(eq_can_to _ _ _ aEb). by apply: Ba xIl _; rewrite (eq_connect aE2b). Qed.
imports: mathcomp(all_ssreflect) extra