proposition: Lemma from_descset_spec d : is_comp_of_n n (if n is 0 then [::] else pairmap (fun a b => b - a) 0 (rcons [seq (val i).+1 | i in d] n)).
proof: Proof. case: n d => // n0; set n' := n0.+1 => d. have Hsort : sorted ltn [seq (val i).+1 | i in d]. rewrite /image_mem /enum_mem -enumT /= sorted_map; apply: sorted_filter. - by move => i j k /= /ltn_trans; apply. - have /eq_sorted-> : relpre nat_of_ord ltn =2 fun i j : 'I_n'.-1 => i < j by []. exact: enum_ord_sorted_ltn. have Hall : all (fun i => 0 < i < n') [seq (val i).+1 | i in d]. by apply/allP => i /mapP/=[[io Hio /= _ ->]]/=; exact: Hio. have {}Hsort : sorted ltn (rcons [seq (val i).+1 | i in d] n'). case: [seq _ | i in _] Hall Hsort => // a l Hall /sorted_rcons; apply. by move: Hall => /allP/(_ _ (mem_last _ _))/andP[_]. rewrite /is_comp_of_n /=. elim/last_ind: [seq _ | i in _] Hsort Hall => [|s sn IHs]/= Hsort Hall. by rewrite addn0 subn0 eqxx. have lt_last : last 0 s < sn. move: Hsort {IHs} => /sorted_rconsK. case/lastP: s Hall => [/andP[/andP[]]// |s sn1 _]. rewrite last_rcons -!cats1 -catA => /cat_sorted2[]/=. by rewrite andbT. have {Hsort}/IHs Hrec : sorted ltn (rcons s n'). case: s Hall Hsort {IHs lt_last} => // a l /allP Hall. move/sorted_rconsK/sorted_rconsK/sorted_rcons; apply. suff /Hall/andP[] : last a l \in rcons (a :: l) sn by []. by rewrite mem_rcons inE mem_last orbT. move: Hall; rewrite all_rcons => /andP[/= /andP[_ lt_sn_n] {}/Hrec/andP[]]. rewrite -!cats1 !pairmap_cat last_cat !sumn_cat /= !addn0 => /eqP Hsum Hcomp. apply/andP; split => [{Hcomp}|{Hsum}]. - rewrite -{2}Hsum -addnA eqn_add2l addnC addnBA //; last exact: ltnW. by rewrite subnK // ltnW. - move: Hcomp; rewrite !is_comp_cat => /andP[-> _]/=. by rewrite !is_comp1 -!lt0n !subn_gt0 lt_last lt_sn_n. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass sorted partition subseq ordtype