proposition: Fact alpha_incr (x : rat) : 0 <= x -> alpha x <= alpha (x + 1).
proof: Proof. move=> le0i; rewrite -subr_ge0; set rhs := (X in 0 <= X). have -> : rhs = (rat_of_Z 51 * x ^+ 4 + rat_of_Z 456 * x ^+ 3 + rat_of_Z 1497 * x ^+ 2 + rat_of_Z 2136 * x + rat_of_Z 1121) / ((x + rat_of_Z 3) ^+ 3 * (x + rat_of_Z 2) ^+ 3). by rewrite /rhs /alpha; field; rewrite !lt0r_neq0 // ltr_wpDl. by rewrite divr_ge0 ?addr_ge0 // mulr_ge0 // exprn_ge0 // addr_ge0. 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