proposition: Lemma inf_alg_proof x : {d | 0 < d & 0 < x -> (d%:RA < x)}.
proof: Proof. have [|] := lerP; first by exists 1. elim/quotW: x=> x; rewrite zeroE=> /lt_algP /= x_gt0. exists (diff x_gt0 / 2%:R); first by rewrite pmulr_rgt0 ?gtr0E ?diff_gt0. rewrite piE -(rwP lt_algP) /= => _; pose_big_enough i. apply: (@lt_crealP _ (diff x_gt0 / 2%:R) i i) => //. by rewrite pmulr_rgt0 ?gtr0E ?diff_gt0. by rewrite -[_ + _](splitf 2) diff0P. by close. Qed.
imports: HB(structures) mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype) mathcomp(bigop order ssralg ssrnum ssrint rat poly polydiv polyorder) mathcomp(perm matrix mxpoly polyXY binomial generic_quotient) mathcomp(cauchyreals separable zmodp bigenough)