proposition: Lemma remark_7_4 : let r := (a i - 1)%N%:Q / (n.+1 - a i)%N%:Q in (exp_quo (n%:Q / (a i)%:Q) n (a i) / exp_quo ((n.+1 - a i)%N%:Q / (a i)%:Q) (n.+1 - a i) (a i)) ^+ a i = exp_quo (1 + r) (n.+1 - a i) (a i) ^+ a i * ((n%:Q / (a i)%:Q) ^ (a i - 1)%N)%:C.
proof: Proof. move => r. have {r} ->: 1 + r = n%:Q / (n.+1 - a i)%N%:Q. by rewrite /r -!subzn //; first field; ring_lia. case: (a i) (a_pos i) Hain => // ai' _ Hain'. rewrite subn1 subSS exprMn exprVn ![exp_quo _ _ _ ^+ ai'.+1]exprAC !rootCK //. rewrite rmorphXn !rmorphM !fmorphV !rmorph_int !exprMn !exprVn !exprnP /=. rewrite -subzn ?expfzDr -?invr_expz ?exprz_pintl; [| ring_lia..]. by field; rewrite !intr_eq0 !expf_eq0; 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