proposition: Lemma order_path_min_in x s : {in P & &, transitive leT} -> all P (x :: s) -> path leT x s -> all (leT x) s.
proof: Proof. move=> leT_tr; elim: s => //= y s ihs /and3P [Px Py Ps] /andP [xy ys]. rewrite xy {}ihs ?Px //=; case: s Ps ys => //= z s /andP [Pz Ps] /andP [yz ->]. by rewrite (leT_tr _ _ _ Py Px Pz). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)