proposition: Lemma ord_path (x y : K) s : ord x y -> path ord y s -> path ord x s.
proof: Proof. elim: s x y=>[|k s IH] x y //=. by move=>H1; case/andP=>H2 ->; rewrite (trans H1 H2). Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun seq path) LemmaOverloading(ordtype prelude)