proposition: Lemma to_algcreal_ofP p c r i j : 0 <= r -> (i <= j)%N -> `|to_algcreal_of p c r j - to_algcreal_of p c r i| <= r * 2%:R ^- i.
proof: Proof. move=> r_ge0 leij; pose r' := r * 2%:R ^- j * (2%:R ^+ (j - i) - 1). apply: le_trans (_ : r' <= _); last first. rewrite /r' -mulrA ler_wpmul2l // ler_pdivr_mull ?exprn_gt0 ?ltr0n //. rewrite -{2}(subnK leij) exprD mulfK ?gt_eqF ?exprn_gt0 ?ltr0n //. by rewrite ger_addl lerN10. rewrite /r' subrX1 addrK mul1r -{1 2}(subnK leij); set f := _ c r. elim: (_ - _)%N=> [|k ihk]; first by rewrite subrr normr0 big_ord0 mulr0 lexx. rewrite addSn big_ord_recl /= mulrDr. rewrite (le_trans (ler_dist_add (f (k + i)%N) _ _)) //. rewrite ler_add ?expr0 ?mulr1 ?to_algcreal_of_recP // (le_trans ihk) //. rewrite exprSr invfM -!mulrA !ler_wpmul2l ?invr_ge0 ?exprn_ge0 ?ler0n //. by rewrite mulr_sumr ler_sum // => l _ /=; rewrite exprS mulKf ?pnatr_eq0. 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)