proposition: Lemma is_parttupleP t : reflect [/\ tnth t ord0 = 0, tnth t ord_max = d, sorted leq t & forall i, 0 < i < d -> (nth 0 t i).*2 >= nth 0 t i.-1 + nth 0 t i.+1] (is_parttuple t).
proof: Proof. apply (iffP and4P) => [[/eqP->/eqP->->/allP Hall] | [->->-> Hall]]. split=> // i Hi; apply: Hall; rewrite mem_iota add1n. by case: d {t} i Hi => [] [|]. split => //; apply/allP => i; rewrite mem_iota add1n => Hi; apply: Hall. by case: d {t} i Hi => [] [|]. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype