proposition: Fact le_1_rho (i : int) : 0 <= i -> 1 <= rho i.
proof: Proof. move=> lei0; rewrite /rho ler_pdivlMr; last exact: lt_0_a. by rewrite mul1r; apply: a_incr; rewrite ler_wpDr. 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