proposition: Lemma a_maj (i : int) : 1 < i -> Posz N_rho + 1 < i -> Ka * 33%:Q ^ i < a i.
proof: Proof. move=> lt1i ltiNrho. rewrite /Ka; set Ka' := (X in a 1 * X * _ <_). suff : Ka' * 33%:Q ^ i < a i / a 1. rewrite [in X in X -> _]ltr_pdivlMr; last exact: lt_0_a. by rewrite mulrC [in X in X -> _]mulrA. rewrite -[X in _ < X](@telescope_prod_int _ 1 i (fun i => a i)) //; last first. by move=> /= k /andP [le1k ltki]; apply/a_neq0/le_trans/le1k. rewrite (big_cat_int _ _ _ _ (ltW ltiNrho)) /=; last by rewrite lerDr. suff hrho_maj : 33%:Q ^ i / 33%:Q ^+ N_rho.+1 < \prod_(Posz N_rho + 1 <= i0 < i :> int) (a (i0 + 1) / a i0). rewrite /Ka' mulrAC -mulrA ltr_pM2l; first exact: hrho_maj. rewrite big_int_cond; apply: prodr_gt0 => j; rewrite andbT => /andP [hj _]. exact/lt_0_rho/le_trans/hj. rewrite -PoszD; case: i lt1i ltiNrho => i //. rewrite !ltz_nat addn1 => lt1i ltiNrho. rewrite eq_big_int_nat /= -expfB // -prodr_const_nat. by apply: ltr_prod_nat=> [// | j /andP[h51j hji]]; rewrite rho_maj 1?h51j. 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