proposition: Lemma path_sorted_inE x s : all P (x :: s) -> path leT x s = all (leT x) s && sorted leT s.
proof: Proof. move=> Pxs; apply/idP/idP => [xs|/andP[/path_min_sorted<-//]]. by rewrite (order_path_min_in leT_tr) //; apply: path_sorted xs. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)