proposition: Lemma itv_o_inftyEbigcup x : `]x, +oo[%classic = \bigcup_k `[x + k.+1%:R^-1, +oo[%classic.
proof: Proof. rewrite predeqE => y; split => [|[n _]]/=. rewrite in_itv /= andbT => xy. have {}[k xky] := ltr_add_invr xy. by exists k => //=; rewrite in_itv /= (ltW xky). rewrite in_itv /= andbT => xny. by rewrite in_itv /= andbT (lt_le_trans _ xny) // ltrDl 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