proposition: Lemma vb_stripP inner outer : is_part inner -> is_part outer -> reflect (forall i, nth 0 inner i <= nth 0 outer i <= (nth 0 inner i).+1) (vb_strip inner outer).
proof: Proof. Proof using. move=> Hinn Hout; apply (iffP idP) => [Hstrip|]. - elim: outer inner Hstrip Hout Hinn => [| out0 out IHout] //= [| inn0 inn]. + by move=> _ _ _ i; rewrite nth_default. + by move => /eqP. + move=> /andP[/eqP-> {out0 IHout} H] _ _ [|i] //=. elim: out H i => [_ i| out1 out IHout] /=. by rewrite nth_default. by move=> /andP[/eqP-> {}/IHout Hrec]; case. + by move=> /andP[H0 {}/IHout Hrec] /andP[Hout {}/Hrec Hrec] /andP[Hinn {}/Hrec Hrec] [|i] //=. - elim: outer inner Hout Hinn => [| out0 out IHout]. + case => //= inn0 inn _ /= /andP[Habs Hinn] H; exfalso. move/(_ 0) : H => /= /andP[]; rewrite leqn0 => /eqP Hinn0 _. by subst inn0; move: Habs Hinn; rewrite leqn0 => /part_head0F ->. + move=> inner Hpart; have:= part_head_non0 Hpart => /=. rewrite -lt0n eqn_leq => H0out. case: inner => [_ {IHout} H | inn0 inn]/=. * rewrite H0out. have:= H 0 => /= -> /=. have {H} /= Hout i := H i.+1. move: Hpart => /= /andP[_]. elim: out Hout => [// | out1 out IHout] H Hpart. have:= part_head_non0 Hpart => /=. rewrite -lt0n eqn_leq => ->. have:= H 0 => /= -> /=. apply: IHout; last exact: (is_part_consK Hpart). by move=> i; exact: H i.+1. * move: Hpart => /andP[H0 {}/IHout Hrec] /andP[_ {}/Hrec Hrec] H. have := H 0 => /= -> /=. apply Hrec => i. exact: H i.+1. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools sorted partition