proposition: Lemma order_path_min x s : transitive leT -> path leT x s -> all (leT x) s.
proof: Proof. by move=> leT_tr; apply/order_path_min_in/all_predT => //; apply: in3W. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)