proposition: Lemma rembigE l s : take (posbig (l :: s)) (l :: s) ++ drop (posbig (l :: s)).+1 (l :: s) = rembig (l :: s).
proof: Proof. Proof using Z. apply/eqP/rembigP; first by []. set ss := l :: s; set pos := posbig (l :: s). exists (take pos ss), (nth Z ss pos), (drop pos.+1 ss); split. - by []. - rewrite [X in _ ++ X](_ : _ = drop pos ss) ?cat_take_drop //. rewrite /ss /pos /= {ss pos}. elim H : s => [//= | s0 s']; rewrite -H. case (boolP (allLtn s l)) => Hmax /=; first by rewrite drop0. move: Hmax; rewrite H => Hmax /=. case (boolP (allLtn s' s0)) => Hmax0 /=; first by rewrite drop0. suff -> : allLtn s' l = false by []. apply: negbTE; move: Hmax; apply: contra => /= Hmax. apply: allLtnCons; last exact Hmax. case: s' Hmax0 Hmax {H} => [//= | s1 s']; rewrite !allLtnConsE. by rewrite -leNgt; apply: le_lt_trans. - by rewrite /ss /pos {ss pos} nth_posbig; apply: allLeq_posbig. - by rewrite /ss /pos {ss pos} nth_posbig; apply: allLtn_posbig. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(order) tools