proposition: Lemma rembigP w wb : wb != [::] -> reflect (exists u b v, [/\ w = u ++ v, wb = u ++ b :: v, allLeq u b & allLtn v b]) (w == rembig wb).
proof: Proof. Proof using. move=> Hwb; apply: (iffP idP). - elim: wb Hwb w => [| w0 wb IHwb _] //= w. case H : (allLtn wb w0) => /eqP->{w}. + by exists [::], w0, wb; rewrite H !cat0s; split. + have Hwb : wb != [::] by move: H; case wb. move Hw : (rembig wb) => w. move: Hw => /esym/eqP/(IHwb Hwb w) [u] [b] [v] [Hcatw Hcatwb Hub Hvb]. exists (w0 :: u), b, v; split. * by rewrite Hcatw. * by rewrite Hcatwb. * move: H; rewrite Hcatwb /= Hub andbT => /negbT. apply: contraR; rewrite -ltNge => Hb. rewrite allLtn_catE /= Hb /=; apply/andP; split. + move: Hub => /allP /= Hub; apply/allP => x Hx /=. exact: (le_lt_trans (Hub x Hx)). + move: Hvb => /allP /= Hvb; apply/allP => x Hx /=. exact: (lt_trans (Hvb x Hx)). * exact: Hvb. - move=> [u] [b] [v] [] {Hwb}. elim: u w wb => [w wb -> -> _ /= -> // | u0 u IHu]. move=> w wb ->{w} ->{wb} Hleqb Hltnb /=. move Hw : (u ++ v) => w; move: Hw => /esym Hw. move Hwb : (u ++ b :: v) => wb; move: Hwb => /esym => Hwb. have:= IHu _ _ Hw Hwb (allLeq_consK Hleqb) Hltnb => /eqP ->. rewrite allLeqConsE in Hleqb. have:= le_trans (maxLb u0 u) Hleqb; rewrite {2}Hwb. case H : (allLtn (u ++ b :: v) u0) => //=. move: H; rewrite allLtn_catE allLtnConsE => /andP[_]. move/(le_lt_trans (maxLb _ _)) => H1 H2. by have:= lt_le_trans H1 H2; rewrite ltxx. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(order) tools