proposition: Lemma sumn_take_pardom_meet i sh1 sh2 : sumn (take i (sh1 `&` sh2)%O) = minn (sumn (take i sh1)) (sumn (take i sh2)).
proof: Proof. case: (ltnP i d.+1) => [lt_i_d1 | le_d_i]. rewrite (sumn_take_part_fromtuple (parttuple_minnP sh1 sh2) lt_i_d1) /=. rewrite (nth_map ord0) ?size_enum_ord //=. rewrite -[i]/(val (Ordinal lt_i_d1)) nth_ord_enum /=. rewrite !(tnth_nth 0) /= ![nth 0 _ _](nth_map ord0) ?size_enum_ord //=. by rewrite -[i]/(val (Ordinal lt_i_d1)) nth_ord_enum /=. rewrite !take_intpartn_over ?(ltnW le_d_i) //. by rewrite !sumn_intpartn minnn. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype