proposition: Fact lt_beta_1 (x : rat) : 0 <= x -> beta x < 1.
proof: Proof. move=> le0i; rewrite /beta expr_lte1 //; last by apply/divr_ge0; apply/addr_ge0. by rewrite ltr_pdivrMr ?ltr_wpDl // mul1r ltrD2l lt_rat_of_Z. 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