proposition: Lemma eqsl_lastR_uniq s x : uniq s -> s = &=s `]-oo, (last x s)].
proof: Proof. move=>U; rewrite /eq_slice /= [LHS]slice_usize index_last_size_uniq // slice_oPR. by case: ifP=>// /negbT; rewrite -ltnNge /= ltnS leqn0 => /eqP/size0nil->. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext slice useqord)