proposition: Lemma tsorted_inv x a l : TS[a, x :: l] -> TS[a, [seq y <- x :: l | ~~ x =[a]= y]].
proof: Proof. move=> [xlSa CR BR]; split => [|y z|y z]. - rewrite /= symconnect0 /=. apply/(subset_trans _ xlSa)/subsetP=> z /=. by rewrite !inE orbC mem_filter => /andP[_ ->]. - rewrite !mem_filter => /andP[xNDy yIxl] yCz. apply/andP; split; last by apply: CR yCz. apply: contra xNDy => xDz. have : C[y]_(a, x :: l) =[x :: l]< x. apply: BR yIxl (connect_trans yCz _). by case/andP: xDz. rewrite /before index_head /=; case: eqP => // -> _. by apply: symconnect_can_to. rewrite !mem_filter => /andP[xNDy yIxl] yCz. have ->: C[y]_(a, [seq i <- x :: l | ~~ x =[a]= i]) = C[y]_(a, x :: l). elim: (x :: l) => //= t l1 IH. case : (boolP (_ =[_]= _)) => Ext /=; last first. by rewrite /can_to /=; case : (boolP (_ =[_]= _)). rewrite IH /can_to /=. case : (boolP (_ =[_]= _)) => Eyt //=. by case/negP: xNDy; apply: symconnect_trans Ext _; rewrite symconnect_sym. apply: before_filter; last by apply: BR. rewrite mem_filter mem_can_to // ?andbT. apply: contra xNDy => xDc. by apply: symconnect_trans xDc (symconnect_can_to _ _ _). Qed.
imports: mathcomp(all_ssreflect) extra