proposition: Lemma Qint_l3b (n : nat) : 2%:Q * (l n)%:Q ^ 3 * b (Posz n) \is a Qint.
proof: Proof. set goal_term := (X in X \is a Qint). have {goal_term} -> : goal_term = 2%:Q * (l n)%:Q ^ 3 * ghn3 n * a n + 2%:Q * (l n)%:Q ^ 3 * (\sum_(0 <= k < Posz n + 1 :> int) c n k * s n k). rewrite -mulrA -mulrDr mulr_sumr -big_split /=; congr (_ * _). by apply: eq_bigr => i _; rewrite mulrC -mulrDr. rewrite mulr_sumr big_int_cond /=. apply/rpredD/rpred_sum. apply/rpredM/Qint_a; rewrite mulr_sumr big_int_cond; apply: rpred_sum. move=> i /andP [/andP [h1i hin] _]; rewrite -mulrA expfV -expfzMl. apply/rpredM/rpredX/iter_lcmn_mul_rat; rewrite // normr_denq denqVz; lia. move=> k /andP [/andP [le0k lekn] _]; rewrite mulrA mulr_sumr big_int_cond /=. apply/rpred_sum => m /andP [/andP [le1m lemk] _]; rewrite -mulrA cdM //. pose hardest_term := (l n)%:Q ^ 3 / (m%:Q ^ 3 * (binomialz k m)%:Q ^ 2). set other_term := (X in _ * _ * _ * X). set goal_term := (X in X \is a Qint). have {goal_term} -> : goal_term = (-1) ^ (m + 1) * other_term * hardest_term. rewrite /goal_term /hardest_term; field. rewrite !intr_eq0 lt0r_neq0 ?binz_gt0; lia. apply/rpredM; first by rewrite expN1r rpred_zify. have {hardest_term other_term} -> : hardest_term = ((l n)%:Q / m%:Q) * ((l n)%:Q / (m * binomialz k m)%:Q) ^ 2. rewrite expfzMl {}/hardest_term; field. by rewrite !intr_eq0 lt0r_neq0 ?binz_gt0; lia. apply/rpredM/rpredX. apply: iter_lcmn_mul_rat; rewrite normr_denq denqVz; lia. case: k m le0k le1m lemk lekn => [] k [] m // *. rewrite binz_nat_nat; apply/Qint_dvdz/dvd_nbin_iter_lcmn; lia. Qed.
imports: mathcomp(all_ssreflect all_algebra) tactics binomialz bigopz arithmetics seq_defs a_props