proposition: Lemma to_algcreal_of_recP p c r i : 0 <= r -> `|to_algcreal_of p c r i.+1 - to_algcreal_of p c r i| <= r * 2%:R ^- i.+1.
proof: Proof. move=> r_ge0 /=; case: ifP=> _; rewrite addrAC subrr add0r ?normrN ger0_norm //; by rewrite mulr_ge0 ?invr_ge0 ?exprn_ge0 ?ler0n. 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)