proposition: Lemma posbig_take_dropE l s : take (posbig (l :: s)) (rembig (l :: s)) ++ maxL l s :: drop (posbig (l :: s)) (rembig (l :: s)) = l :: s.
proof: Proof. Proof using. elim Hs : s l => [// | s0 s' IHs] l; rewrite -Hs /=. case/boolP: (allLtn s l) => Hl /=. - by rewrite take0 drop0 /=; have:= (allLtnW Hl) => /allLeqE ->. - move: Hl; rewrite Hs allLtnConsE -leNgt /= -maxXL => /max_idPr ->. by rewrite (IHs s0). Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(order) tools