proposition: Lemma posbigE u b v : (allLeq u b && allLtn v b) = (posbig (u ++ b :: v) == size u).
proof: Proof. Proof using. apply/andP/idP => [[Hu Hv]|]. - elim: u Hu => [| u0 u IHu] /=; first by rewrite Hv. move=> /andP[Hub Hall]; rewrite allLtn_catE /= ltNge Hub andbF eqSS. exact: IHu. - elim: u => [/= | u0 u /= IHu]; first by case (allLtn v b). case/boolP: (allLtn (u ++ b :: v) u0) => [| Hall] //=. rewrite eqSS => {}/IHu [Hub Hvb]. split; last exact: Hvb. rewrite Hub andbT. move: Hall; apply: contraR; rewrite -ltNge => H. rewrite allLtn_catE /= H /=. apply/andP; split; apply/allP => x. + by move: Hub => /allP/[apply] /= H1; apply: (le_lt_trans H1 H). + by move: Hvb => /allP/[apply] /= H1; apply: (lt_trans H1 H). Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(order) tools