proposition: Lemma sorted_slt ks : uniq ks -> sorted (seq_lt ks) ks.
proof: Proof. case: ks=>//= k ks; elim: ks k=>[|k1 ks IH] k2 //=. rewrite inE negb_or -andbA=>/and4P [N1 N2 N3 N4]. rewrite sltL eq_sym N1 /=. have : path (seq_lt [:: k1 & ks]) k1 ks by apply: IH; rewrite N3 N4. apply: (@sub_in_path _ (mem (k1::ks))); last by apply/allP. move=>x y /=; rewrite !inE !slt_cons. case/orP=>[/eqP ->{x}|X]. - rewrite (eq_sym k1 k2) (negbTE N1) /= eq_refl andbT. case/orP=>[/eqP ->|Y ->]; first by rewrite eq_refl. by case: eqP Y N2=>// ->->. case/orP=>[/eqP ->|Y]; first by rewrite eq_refl. case: eqP Y N3=>[->|/eqP N Y N3] //=. case: eqP X N3=>[->->|/eqP M X K1] //= H. by rewrite H orbT andbT; case: eqP Y N2=>// ->->. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext)