proposition: Lemma sorted_lt_by_pos r p q : sorted r -> p < size r -> q < size r -> (nth Z r p != nth Z r q) && (nth Z r p <=R nth Z r q) -> p < q.
proof: Proof. Proof using Hanti Rrefl Rtrans. move=> /sorted2P Hsort Hp Hq /andP[Hneq Hpq]. have H : q <= p -> (nth Z r q <=R nth Z r p). by move=> Hqp; apply Hsort; rewrite Hqp Hp. have:= contra H; rewrite ltnNge; apply. apply/negP => Hqp. move: Hneq; suff -> : nth Z r p = nth Z r q by rewrite eq_refl. by apply Hanti; rewrite Hqp Hpq. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun ssrnat eqtype fintype choice seq) mathcomp(path)