proposition: Lemma path_all (xs : seq A) x r : transitive r -> path r x xs -> all (r x) xs.
proof: Proof. by move=>Ht; rewrite path_sortedE; [case/andP | exact: Ht]. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq eqtype path fintype finfun tuple interval perm fingroup) pcm(options prelude ordtype seqext slice)