proposition: Lemma bigmaxR_undup (I : eqType) g : forall (s : seq I), \rmax_(c <- s) g c = \rmax_(c <- undup s) g c.
proof: Proof. elim=> // hd tl IH /=. rewrite big_cons. case: ifP => Hcase. - rewrite -IH Rmax_right //; exact: leR_bigmaxR. - by rewrite big_cons IH. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) Reals mathcomp(lra) mathcomp(Rstruct)