proposition: Lemma sorted_sumn_iotaE s : sorted ltn s -> sumn s = sumn (iota 0 (size s)) -> s = iota 0 (size s).
proof: Proof. elim/last_ind: s => [//= | s sn IHs] /= Hsort. have:= sorted_ltn_ind Hsort. rewrite -{2 5}(revK (rcons s sn)) rev_rcons sumn_rev /= [sn + _]addnC sumn_rev. rewrite size_rcons -{1 3 4}addn1 iotaD /= sumn_cat /= add0n addn0 cats1. rewrite last_rcons => [] [_ Hsn]. have [Hsum _] := sorted_ltn_ind (sorted_rconsK Hsort). by move=> /esym/(leq_addE Hsum Hsn) [/esym/(IHs (sorted_rconsK Hsort)) <- <-]. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun ssrnat eqtype fintype choice seq) mathcomp(path) tools