proposition: Lemma notin_path (x : K) s : path ord x s -> x \notin s.
proof: Proof. elim: s=>[|k s IH] //=. rewrite inE negb_or; case/andP=>T1 T2; case: eqP=>H /=. - by rewrite H irr in T1. by apply: IH; apply: ord_path T2. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path) pcm(options)