proposition: Lemma lt_33_r51 : rat_of_Z 33 < rho (Posz 51).
proof: Proof. by rewrite rho_h_iter // [_ < _]refines_eq; vm_compute. 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