proposition: Lemma trivIset_is_max_approxRN n : trivIset [set: nat] (E n).
proof: Proof. apply/trivIsetP => /= i j _ _ ij. apply/seteqP; split => // x []; rewrite /E/= => -[+ + [+ +]]. wlog : i j ij / (i < j)%N. move=> h Fmgi iFm Fmgj jFm. have := ij; rewrite neq_lt => /orP[ji|ji]; first exact: (h i j). by apply: (h j i) => //; rewrite eq_sym. by move=> {}ij Fmgi h Fmgj => /(_ _ ij); rewrite -Fmgi -Fmgj ltxx. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum ssrint interval) mathcomp(finmap fingroup perm rat) mathcomp(mathcomp_extra boolp classical_sets cardinality) mathcomp(functions fsbigop set_interval) HB(structures) reals ereal signed topology numfun normedtype sequences esum measure realfun lebesgue_measure lebesgue_integral