proposition: Lemma leq_head_sumn sh : head 0 sh <= sumn sh.
proof: Proof. by case: sh => //= s0 s; apply: leq_addr. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype