proposition: Lemma set_lte_bigcup : [set x | f x > g x] = \bigcup_j E j.
proof: Proof. apply/seteqP; split => [x/=|x [n _]]; last first. by rewrite /E/= -sube_gt0; apply: lt_le_trans. move gxE : (g x) => gx; case: gx gxE => [gx| |gxoo fxoo]; last 2 first. - by case: (f x). - by exists 0%N => //; rewrite /E/= gxoo addey// ?leey// -ltNye. move fxE : (f x) => fx; case: fx fxE => [fx fxE gxE|fxoo gxE _|//]; last first. by exists 0%N => //; rewrite /E/= fxoo gxE// addye// leey. rewrite lte_fin -subr_gt0 => fgx; exists `|floor (fx - gx)^-1%R|%N => //. rewrite /E/= -natr1 natr_absz ger0_norm ?floor_ge0 ?invr_ge0; last exact/ltW. rewrite fxE gxE lee_fin -[leRHS]invrK lef_pV2//. - by apply/ltW; rewrite lt_succ_floor. - by rewrite posrE// ltr_pwDr// ler0z floor_ge0 invr_ge0 ltW. - by rewrite posrE invr_gt0. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum ssrint interval) mathcomp(finmap fingroup perm rat) mathcomp(mathcomp_extra boolp classical_sets functions) HB(structures) reals ereal signed topology normedtype sequences