proposition: Lemma allLtn_posbig l s : allLtn (drop (posbig (l :: s)).+1 (l :: s)) (maxL l s).
proof: Proof. Proof using. elim Hs : s l => [// | s0 s'] IHs l; rewrite -Hs /=. move/(_ (Order.max l s0)) : IHs; rewrite /= maxC /Order.max. case: (ltP s0 l) => Hs0; rewrite Hs /=. - rewrite Hs0 /=; have:= ltW Hs0 => /max_idPl ->. case (boolP (allLtn s' l)) => Hall. + rewrite drop0 /= => ->. have /allLeqE -> := allLtnW Hall. by rewrite Hs0. + suff -> : allLtn s' s0 = false by []. apply: negbTE; move: Hall; apply: contra; apply: sub_all => i /= Hi. exact: (lt_trans Hi). - rewrite ltNge Hs0 /=. by move: Hs0 => /max_idPr ->. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(order) tools