proposition: Lemma bigmaxR_seq_eq (A : finType) (f : A -> R) (s : seq A) a : a \in s -> (forall a0, 0 <= f a0) -> (forall a0, a0 \in s -> f a0 <= f a) -> f a = \rmax_(a0 <- s) f a0.
proof: Proof. elim: s a => // hd tl IH a; rewrite in_cons; case/orP. - move/eqP => -> Hhpos Hh. rewrite big_cons. rewrite Rmax_left //. apply leR_bigmaxRl => //. move=> c0 Hc0; apply Hh. by rewrite in_cons Hc0 orbC. - move=> atl Hhpos Hh. rewrite big_cons Rmax_right //. + apply IH => //. move=> c0 Hc0; apply Hh. by rewrite in_cons Hc0 orbC. + rewrite -(IH a) //. * apply Hh. by rewrite in_cons eqxx. * move=> c0 Hc0. apply Hh. by rewrite in_cons Hc0 orbC. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) Reals mathcomp(lra) mathcomp(Rstruct)