proposition: Lemma ltr_add_invr (y x : R) : y < x -> exists k, y + k.+1%:R^-1 < x.
proof: Proof. move=> yx; exists `|floor (x - y)^-1|%N. rewrite -ltrBrDl -{2}(invrK (x - y)%R) ltf_pV2 ?qualifE/= ?ltr0n//. by rewrite invr_gt0 subr_gt0. rewrite -natr1 natr_absz ger0_norm. by rewrite floor_ge0 invr_ge0 subr_ge0 ltW. by rewrite -RfloorE lt_succ_Rfloor. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra) mathcomp(mathcomp_extra boolp classical_sets set_interval) Setoid