proposition: Lemma a_asympt (n : nat) : (N_rho + 1 < n)%N -> 1 / a n < Ka^-1 / 33%:Q ^ n.
proof: Proof. move=> hn; rewrite ltr_pdivrMr; last exact: lt_0_a. rewrite -invfM ltr_pdivlMl; last exact/mulr_gt0/exprz_gt0/isT/lt_0_Ka. by rewrite mulr1; apply/a_maj/hn/leq_trans/hn. 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