proposition: Lemma delta_incr (x : rat) : 0 <= x -> delta x <= delta (x + 1).
proof: Proof. move=> le0x; rewrite -subr_ge0; set rhs := (X in 0 <= X). have -> : rhs = (rat_of_Z 3456 * x ^ 10 + rat_of_Z 77550 * x ^ 9 + rat_of_Z 777825 * x ^ 8 + rat_of_Z 4591644 * x ^ 7 + rat_of_Z 17666100 * x ^ 6 + rat_of_Z 46291464 * x ^ 5 + rat_of_Z 83678475 * x ^ 4 + rat_of_Z 103061566 * x ^ 3 + rat_of_Z 82798770 * x ^ 2 + rat_of_Z 39197496 * x + rat_of_Z 8307151) / ((x + rat_of_Z 3) ^ 6 * (x + rat_of_Z 2) ^ 6). rewrite {}/rhs /delta /alpha /beta. by 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