proposition: Lemma vb_strip_conj inner outer : is_part inner -> is_part outer -> vb_strip inner outer -> hb_strip (conj_part inner) (conj_part outer).
proof: Proof. Proof using. move=> Hinn Hout. have Hcinn := is_part_conj Hinn; have Hcout := is_part_conj Hout. move => /(vb_stripP Hinn Hout) H. apply/(hb_stripP Hcinn Hcout) => i; rewrite -!conj_leqE //. apply/andP; split. + move/(_ (nth 0 (conj_part inner) i)) : H => /andP[_ /leq_trans]. by apply; rewrite ltnS conj_leqE. + move/(_ (nth 0 (conj_part outer) i)) : H => /andP[/leq_trans H _]. by apply H; rewrite conj_leqE. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools sorted partition