proposition: Lemma lee_mul01Pr x y : 0 <= x -> reflect (forall r, (0 < r < 1)%R -> r%:E * x <= y) (x <= y).
proof: Proof. move=> x0; apply/(iffP idP) => [xy r /andP[r0 r1]|h]. move: x0 xy; rewrite le_eqVlt => /predU1P[<-|x0 xy]; first by rewrite mule0. by rewrite (le_trans _ xy) // gee_pmull // ltW. have h01 : (0 < (2^-1 : R) < 1)%R by rewrite invr_gt0 ?invf_lt1 ?ltr0n ?ltr1n. move: x y => [x||] [y||] // in x0 h *. - move: (x0); rewrite lee_fin le_eqVlt => /predU1P[<-|{}x0]. by rewrite (le_trans _ (h _ h01))// mule_ge0// lee_fin. have y0 : (0 < y)%R. by rewrite -lte_fin (lt_le_trans _ (h _ h01))// mule_gt0// lte_fin. rewrite lee_fin leNgt; apply/negP => yx. have /h : (0 < (y + x) / (2 * x) < 1)%R. apply/andP; split; first by rewrite divr_gt0 // ?addr_gt0// ?mulr_gt0. by rewrite ltr_pdivrMr ?mulr_gt0// mul1r mulr_natl mulr2n ltrD2r. rewrite -(EFinM _ x) lee_fin invrM ?unitfE// ?gt_eqF// -mulrA mulrAC. by rewrite mulVr ?unitfE ?gt_eqF// mul1r; apply/negP; rewrite -ltNge midf_lt. - by rewrite leey. - by have := h _ h01. - by have := h _ h01; rewrite mulr_infty sgrV gtr0_sg // mul1e. - by have := h _ h01; rewrite mulr_infty sgrV gtr0_sg // mul1e. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed