proposition: Lemma prod_is_exp_sum (n k : nat) (tenn := (10 * n)%N%:Q) : \prod_(i < k.+1) exp_quo tenn (a i).-1 (a i) = tenn%:C ^+ k * exp_quo tenn 1 (a k.+1 - 1).
proof: Proof. elim: k => [|k ihk]; first by rewrite expr0 big_ord_recr big_ord0. have pos_tenn : 0 <= tenn by rewrite /tenn ler0n. have h l : tenn%:C ^+ l = exp_quo tenn l 1 by rewrite -exp_quo_r_nat -!CratrE. rewrite big_ord_recr ihk /= !h !subn1 -!exp_quo_plus ?ltnS ?muln_gt0 ?a_pos //=. congr exp_quo; lia. Qed.
imports: ZArith mathcomp(all_ssreflect all_algebra all_field) extra_mathcomp tactics binomialz floor arithmetics posnum rat_of_Z hanson_elem_arith hanson_elem_analysis