proposition: Lemma expR_total_gt1 x : 1 <= x -> exists y, [/\ 0 <= y, 1 + y <= x & expR y = x].
proof: Proof. move=> x_ge1; have x_ge0 : 0 <= x by apply: le_trans x_ge1. have [x1 x1Ix| |x1 _ /eqP] := @IVT _ (fun y => expR y - x) _ _ 0 x_ge0. - apply: continuousB => // y1; last exact: cst_continuous. by apply/continuous_subspaceT=> ?; exact: continuous_expR. - rewrite expR0; have [_| |] := ltrgtP (1- x) (expR x - x). + by rewrite subr_le0 x_ge1 subr_ge0 (le_trans _ (expR_ge1Dx _)) ?lerDr. + by rewrite ltrD2r expR_lt1 ltNge x_ge0. + rewrite subr_le0 x_ge1 => -> /=; rewrite subr_ge0. by rewrite (le_trans _ (expR_ge1Dx x_ge0)) ?lerDr. - rewrite subr_eq0 => /eqP x1_x; exists x1; split => //. + by rewrite -ler_expR expR0 x1_x. + by rewrite -x1_x expR_ge1Dx // -ler_expR x1_x expR0. Qed.
imports: mathcomp(all_ssreflect ssralg ssrint ssrnum matrix) mathcomp(interval rat) mathcomp(boolp classical_sets functions) mathcomp(mathcomp_extra) reals ereal signed topology normedtype landau sequences derive realfun itv convex