proposition: Lemma sorted_ltn_ind s : sorted ltn s -> sumn (iota 0 (size s)) <= sumn s /\ last 0 s >= (size s).-1.
proof: Proof. elim/last_ind: s => [//=| s sn IHs] /= Hsort. move/(_ (sorted_rconsK Hsort)): IHs => [Hsum Hlast]; split. - rewrite -{2}(revK (rcons s sn)) rev_rcons sumn_rev /= [sn + _]addnC sumn_rev. rewrite size_rcons -addn1 iotaD /= sumn_cat /= add0n addn0. apply (leq_add Hsum). case/lastP: s Hsort Hlast {Hsum} => [//= | s sn1] /=. rewrite !size_rcons !last_rcons /= -!cats1 -catA cat1s => /cat_sorted2[_]/=. by rewrite andbT => /(leq_ltn_trans _); apply. - case/lastP: s Hsort Hlast {Hsum} => [//= | s sn1] /=. rewrite !size_rcons !last_rcons /= -!cats1 -catA cat1s => /cat_sorted2[_]/=. by rewrite andbT => /(leq_ltn_trans _); apply. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun ssrnat eqtype fintype choice seq) mathcomp(path) tools