proposition: Lemma bigmaxe_fin_num (s : seq R) r : r \in s -> \big[maxe/-oo%E]_(i <- s) i%:E \is a fin_num.
proof: Proof. move=> rs; have {rs} : s != [::]. by rewrite -size_eq0 -lt0n -has_predT; apply/hasP; exists r. elim: s => [//|a l]; have [-> _ _|_ /(_ isT) ih _] := eqVneq l [::]. by rewrite big_seq1. by rewrite big_cons {1}/maxe; case: (_ < _)%E. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed