proposition: Lemma nth_posbig l s : nth Z (l :: s) (posbig (l :: s)) = maxL l s.
proof: Proof. Proof using. rewrite /=; case: (boolP (allLtn s l)). - by move/allLtnW/allLeqP => ->. - elim Hs : s l => [| s0 s' IHs] //= l. rewrite maxC /Order.max. case: (ltP s0 l) => Hl /= H. + rewrite -(IHs l H). suff -> : allLtn s' s0 = false by []. apply: negbTE; move: H; apply: contra; apply: sub_all => i /= Hi. exact: (lt_trans Hi). + case/boolP: (allLtn s' s0) => /= [|Hs0]. * by move /allLtnW/allLeqP ->. * exact: (IHs s0 Hs0). Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(order) tools