proposition: Fact lt_0_beta (x : rat) : 0 <= x -> 0 < beta x.
proof: Proof. by move=> le0i; apply/exprn_gt0/divr_gt0; apply/ltr_wpDl. 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