proposition: Lemma sorted2P r : reflect (forall (i j : nat), i <= j < (size r) -> (nth Z r i <=R nth Z r j)) (sorted r).
proof: Proof. Proof using Rrefl Rtrans. by apply/(iffP idP); rewrite non_decr_equiv => /(sortedP Z). Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun ssrnat eqtype fintype choice seq) mathcomp(path)