proposition: Lemma sorted_geq_nth0E (s : seq nat) : sorted geq s -> nth 0 s 0 = \max_(i <- s) i.
proof: Proof. case: s => [|s0 s]/= Hpath; first by rewrite big_nil. rewrite big_cons; apply/esym/maxn_idPl. elim: s s0 Hpath => [|s1 s IHs] s0 /=; first by rewrite big_nil. rewrite big_cons geq_max=> /andP[le10 Hpath]. by rewrite le10 /=; apply: (leq_trans _ le10); apply: IHs. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype