proposition: Fact lt_0_delta (x : rat) : 0 <= x -> 0 < delta x.
proof: Proof. move=> le0x; rewrite /delta subr_gt0. have /lt_trans -> //: rat_of_Z 4 * beta x < rat_of_Z 4. by rewrite gtr_pMr // lt_beta_1. have -> : rat_of_Z 4 = rat_of_Z 2 ^+ 2 by ring. rewrite -subr_gt0 subr_sqr mulr_gt0 //. rewrite subr_gt0; exact: lt_2_alphaN. by rewrite addr_gt0 ?lt_0_alpha. 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