proposition: Fact lt_2_alphaN (x : rat) : 0 <= x -> rat_of_Z 2 < alpha x.
proof: Proof. move=> le0i; rewrite /alpha. have npos : 0 < x + rat_of_Z 2 by apply: ltr_wpDl; rewrite ?ler0z. rewrite ltr_pdivlMr; last by apply: exprn_gt0. have trans: rat_of_Z 2 * (x + rat_of_Z 2) ^+ 3 <= rat_of_Z 2 * (x + rat_of_Z 2) ^+ 2 * (rat_of_Z 2 * x + rat_of_Z 3). rewrite [_ ^+ 3]exprSr mulrA ler_wpM2l //. by rewrite mulr_ge0 // exprn_ge0 // addr_ge0. by apply: lerD (ler_peMl _ _) _ => //; ring_lia. apply: le_lt_trans trans _. suff trans : rat_of_Z 2 * (x + rat_of_Z 2) ^+ 2 < rat_of_Z 17 * x ^ 2 + rat_of_Z 51 * x + rat_of_Z 39. by rewrite ltr_pM2r // ltr_wpDl // mulr_ge0. rewrite -exprnP sqrrD !mulrDr; apply: ler_ltD; last first. by rewrite [_ < _]refines_eq. apply: lerD; first by rewrite ler_wpM2r ?exprn_ge0 // [_ <= _]refines_eq. by rewrite [x * _]mulrC mulrA -mulrDl ler_wpM2r // [_ <= _]refines_eq. Qed.
imports: BinInt mathcomp(all_ssreflect all_algebra) mathcomp(realalg) CoqEAL(hrel param refinements) CoqEAL(pos binnat binint rational) tactics shift binomialz bigopz rat_of_Z rho_computations seq_defs c_props initial_conds algo_closures