proposition: Lemma sorted_subseq_iota_rcons s n : subseq s (iota 0 n) = sorted ltn (rcons s n).
proof: Proof. apply/idP/idP. - move=> Hsubs. apply: (subseq_sorted ltn_trans (s2 := (iota 0 n.+1))). + by rewrite -addn1 iotaD add0n /= cats1 -subseq_rcons_eq. + exact: iota_ltn_sorted. - elim: n s => [/= [// | s0 s] | n IHn s]. rewrite rcons_cons /= => /(order_path_min ltn_trans) /= /allP Hall. exfalso. suff /Hall : 0 \in rcons s 0 by []. by rewrite mem_rcons inE eq_refl. case/lastP: s => [_| s sn]; first exact: sub0seq. case: (ltnP sn n) => Hsn. + move/sorted_rconsK => Hsort. have:= Hsn; rewrite -{1}(last_rcons n s sn) => /(sorted_rcons Hsort)/IHn. move/subseq_trans; apply. rewrite -addn1 iotaD add0n cats1. exact: subseq_rcons. + move=> Hsort; have H : sn = n. apply anti_leq; rewrite Hsn andbT. move: Hsort. rewrite -!cats1 -catA => /cat_sorted2/=[]. by rewrite ltnS andbT. subst sn. rewrite -addn1 iotaD add0n /= cats1. rewrite -subseq_rcons_eq; apply IHn. exact: (sorted_rconsK Hsort). Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass sorted