proposition: Lemma sortedP T x (s : seq T) (r : rel T) : reflect (forall i, i.+1 < size s -> r (nth x s i) (nth x s i.+1)) (sorted r s).
proof: Proof. elim: s => [|y [|z s]//= IHs]/=; do ?by constructor. apply: (iffP andP) => [[ryz rzs] [|i]// /IHs->//|rS]. by rewrite (rS 0); split=> //; apply/IHs => i /(rS i.+1). Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra all_solvable) mathcomp(all_field)