proposition: Lemma nth_part_non0 sh i : is_part sh -> i < size sh -> nth 0 sh i != 0.
proof: Proof. by move/in_part_non0 => H le_i_sz; apply/H/mem_nth. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype