proposition: Lemma path_le x x' s : leT x x' -> path leT x' s -> path leT x s.
proof: Proof. by case: s => [//| x'' s xlex' /= /andP[x'lex'' ->]]; rewrite (leT_tr xlex'). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)