proposition: Lemma subdescsetP c1 c2 : reflect (exists2 c : seq (seq nat), c1 = map sumn c :> seq nat & c2 = flatten c :> seq nat) (descset c1 \subset descset c2).
proof: Proof. apply (iffP (subdescset_partsumP c1 c2)) => [| [s Hc1 ->{c2}]]. - case: c1 c2 => [u /andP[/eqP Hu Hcompu]] [v /andP[/eqP Hsum Hcompv]] /=. rewrite -{}Hu in Hsum. elim: u v Hcompu Hcompv Hsum => [| u0 u IHu] v. by move=> _ Hcompv /(comp0 Hcompv) -> _; exists [::]. rewrite is_comp_cons => /andP[Hu0 Hcompu]. case: u IHu Hcompu => [_ _ |u1 u']. rewrite /= addn0 => _ Hv _. by exists [:: v]; rewrite /= ?Hv ?cats0. move Hu : (u1 :: u') => u IHu Hcompu. have uneq0 : u != [::] by rewrite -Hu. have u0in : u0 \in partsums (u0 :: u) by rewrite partsums_cons //= inE eqxx. have [sz] := ubnPeq (size v). elim: sz v => [|sz IHv] [_ |v0 [| v1 v']] //. + by rewrite /= => _ /esym/eqP; rewrite addn_eq0 (negbTE Hu0). + by move=> _ _ _ /(_ _ u0in). move Hv : (v1 :: v') => v; rewrite /= eqSS => /eqP Hsz. have vneq0 : v != [::] by rewrite -Hv. rewrite is_comp_cons => /andP[Hv0 Hcompv] /= Hsum Hsubset. have : v0 <= u0. have {IHu IHv} := Hsubset _ u0in. rewrite partsums_cons // inE => /orP[/eqP ->// | /mapP[x _ ->]]. exact: leq_addr. rewrite leq_eqVlt => /orP[/eqP Heq {IHv} | lt0 {IHu}]. subst v0. move: Hsum => /eqP; rewrite eqn_add2l => /eqP{}/(IHu _ Hcompu Hcompv) Hrec. suff /Hrec [s -> ->] : {subset partsums u <= partsums v}. by exists ([:: u0] :: s); rewrite //= addn0. rewrite -Hu => i Hi {IHu Hrec}. have Hu' := mem_partsum_non0 Hi. have {}/Hsubset : u0 + i \in partsums (u0 :: u). by rewrite partsums_cons // inE map_f ?orbT // -Hu. rewrite partsums_cons // inE => /orP[Heq|]; first last. by rewrite mem_map // => x y /eqP; rewrite eqn_add2l => /eqP. exfalso. move: Heq; rewrite -{2}(addn0 u0) eqn_add2l => /eqP Heq; subst i. have Hcompsu : is_comp_of_n (sumn u) u. by rewrite /is_comp_of_n /= eqxx Hcompu. have /= /allP := all_partsums (IntCompN Hcompsu). by rewrite -Hu => /(_ _ Hi). have {}/IHv Hrec: size ((v0 + v1) :: v') == sz by rewrite -Hsz -Hv. have {}/Hrec Hrec : is_comp (v0 + v1 :: v'). move: Hcompv; rewrite -Hv !is_comp_cons addn_eq0 negb_and orbC. by move=> /andP[/negbTE->->]. have {}/Hrec Hrec : sumn (v0 + v1 :: v') = sumn (u0 :: u). by rewrite /= -Hsum -Hv /= addnA. have {Hsubset}/Hrec : {subset partsums (u0 :: u) <= partsums (v0 + v1 :: v')}. move: Hsubset {Hrec}; rewrite partsums_cons // => Hsub i Hin. have := Hin; rewrite inE => /orP[/eqP Heq | Hin']. subst i; have {Hsub Hin}:= Hsub _ Hin. by rewrite -Hv; exact: (mem_partsum_gt lt0). move: Hin' Hin => /mapP[j jin ->{i} /Hsub]. by rewrite -Hv; apply: (mem_partsum_gt (leq_trans lt0 (leq_addr _ _))). move=> [[| [|p0 p] s]]//= [u0eq ueq]; first by rewrite u0eq in Hu0. move=> [Hp0 Hv']; subst p0 v' u u0 v. by exists ((v0 :: v1 :: p) :: s); rewrite //= -ueq addnA. - have : [::] \notin s. apply/negP => Hs; case: c1 Hc1 => [c1 /= /andP[_ Hcomp Hc1]]. by move: Hcomp; rewrite {}Hc1 /is_comp -[0]/(sumn [::]) map_f. rewrite {c1}Hc1. elim: s => // s0 s IHs; rewrite inE negb_or => /andP[Hs0 Hin]. move/(_ Hin) in IHs. case: s0 Hs0 => //= i s0 _. elim: s0 i => [|c0 c IHc] /= i. rewrite addn0; case: (s =P [::]) => [->// | Hs]. rewrite !partsums_cons; first last. + by move: Hs; apply contra_notN; case s. + by move: Hs {IHs}; apply contra_notN; case: s Hin => // [[|t0 t']]. move=> k; rewrite !inE => /orP[/eqP->|]; first by rewrite eqxx. by move=> /mapP[l /IHs Hl ->{k}]; rewrite map_f // orbT. rewrite addnA [X in {subset _ <= X}]partsums_cons //. move=> k; rewrite !inE => {}/IHc. case: (c =P [::]) => [->{c} | Hc]/=. move=> /mapP[[|l]]; rewrite mem_iota //= add1n ltnS => Hl ->{k}. rewrite -addnA map_f ?orbT // partsums_cons; last by case: (flatten s) Hl. case: l Hl => // l; first by rewrite take0 /= addn0 inE eqxx. move=> Hl; rewrite inE map_f ?orbT //. rewrite /partsums; apply (@map_f _ _ (fun i => sumn (take i (flatten s)))). by rewrite mem_iota add1n; case: (size _) Hl. rewrite !partsums_cons //; try by case: c Hc. rewrite /= !inE => /orP[/eqP ->|]; first by rewrite eqxx orbT. move=> /mapP[l Hl ->{k}]; rewrite orbA; apply/orP; right. by rewrite -map_comp -addnA (@map_f _ _ ([eta addn i] \o [eta addn c0])). Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass sorted partition subseq ordtype