proposition: Lemma itv_c_inftyEbigcap x : `[x, +oo[%classic = \bigcap_k `]x - k.+1%:R^-1, +oo[%classic.
proof: Proof. rewrite predeqE => y; split=> /= [|xy]. rewrite in_itv /= andbT => xy z _ /=; rewrite in_itv /= andbT ltrBlDr. by rewrite (le_lt_trans xy) // ltrDl invr_gt0 ltr0n. rewrite in_itv /= andbT leNgt; apply/negP => yx. have {}[k ykx] := ltr_add_invr yx. have {xy}/= := xy k Logic.I. by rewrite in_itv /= andbT; apply/negP; rewrite -leNgt lerBrDr ltW. 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