proposition: Lemma eq_interv_part sh st1 st2 v : is_part sh -> nth 0 sh st1.+1 <= st1 + v <= nth 0 sh st1 -> nth 0 sh st2.+1 <= st2 + v <= nth 0 sh st2 -> st1 = st2.
proof: Proof. wlog H12 : st1 st2 / st1 <= st2. move=> Hwlog; case: (leqP st1 st2); first exact: Hwlog. by move=> /ltnW/Hwlog H +{}/H => +H => {}/H /(_ _)/esym. move=> /is_part_ijP[_ psh] /andP[Hs1 _] /andP[_ H2s]. apply anti_leq; rewrite H12 /= -(leq_add2r v). move: H12; rewrite leq_eqVlt => /orP[/eqP -> // | lt12]. exact: (leq_trans H2s (leq_trans (psh _ _ lt12) Hs1)). Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools sorted partition