proposition: Lemma part_nseq1P x0 sh : is_part sh -> head x0 sh <= 1 -> sh = nseq (sumn sh) 1.
proof: Proof. move=> Hpart. elim: sh Hpart (part_head_non0 Hpart) x0 => [//|s0 s IHs]/=/andP[H Hpart]. rewrite -lt0n => lt0s0 x0 les01; move: H. have {lt0s0 les01} -> : s0 = 1 by apply anti_leq; rewrite lt0s0 les01. move=> Hhead; rewrite /= -(IHs _ _ 1) //. exact: part_head_non0. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype