proposition: Lemma hb_stripP inner outer : is_part inner -> is_part outer -> reflect (forall i, nth 0 outer i.+1 <= nth 0 inner i <= nth 0 outer i) (hb_strip inner outer).
proof: Proof. Proof using. move=> Hinn Hout; apply (iffP idP). - elim: inner outer {Hinn Hout} => [| inn0 inn IHinn] /= [| out0 out] //=. by move=> /eqP -> i; rewrite leqnn /= nth_default. by move=> /andP[H0 /IHinn{IHinn}Hrec] [// | i]; exact: Hrec. - elim: inner Hinn outer Hout => [| inn0 inn IHinn] Hinn /= [| out0 out] Hout //= H. + have:= H 0 => /andP[]; rewrite nth_nil leqn0 => /eqP {}H _. have:= part_head_non0 (is_part_consK Hout). by rewrite -nth0; case: out H {Hout} => //= out1 out' ->. + move/part_head_non0 : Hinn; move/(_ 0) : H. by rewrite /= leqn0 => ->. + have:= H 0; rewrite nth0 /= => -> /=. apply (IHinn (is_part_consK Hinn) _ (is_part_consK Hout)) => i. exact: H i.+1. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools sorted partition