proposition: Lemma parttuple_minnP sh1 sh2 : is_parttuple (parttuple_minn sh1 sh2).
proof: Proof. have /is_parttupleP[t10 t1d /(sortedP 0) sort1 conv1] := parttupleP sh1. have /is_parttupleP[t20 t2d /(sortedP 0) sort2 conv2] := parttupleP sh2. rewrite size_tuple in sort1; rewrite size_tuple in sort2. apply/is_parttupleP; split. - by rewrite !tnth_mktuple /= !take0. - by rewrite tnth_mktuple t1d t2d minnn. - apply/(sortedP 0) => i {conv1 conv2}; rewrite size_tuple => lti1d1. have ltid1 : i < d.+1 by apply: ltnW. move: sort2 => /(_ _ lti1d1); move: sort1 => /(_ _ lti1d1). rewrite !nth_parttuple_minn // !nth_parttuple // !leq_min !geq_min => -> ->. by rewrite orbT. - move=> i Hi; move: conv2 => /(_ _ Hi); move: conv1 => /(_ _ Hi). case: i Hi => [|i]// /andP[_]; rewrite -ltnS => lti2d1. have lti1d1 : i.+1 < d.+1 by apply: ltnW. have ltid1 : i < d.+1 by apply: ltnW. rewrite !nth_parttuple_minn // !nth_parttuple //= => conv1 conv2. rewrite double_minn !leq_min; apply/andP; split. - by apply: (leq_trans (leq_add _ _) conv1); apply: geq_minl. - by apply: (leq_trans (leq_add _ _) conv2); apply: geq_minr. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype