proposition: Lemma remark_t2_2 k1: \prod_(i < k1) exp_quo (a i)%:Q (a i).-1 (a i) = (\prod_(i < k1) (a i)%:~R) / w_seq k1.
proof: Proof. rewrite -prodfV -big_split /=; apply: eq_bigr => i _. by rewrite /a' /exp_quo -subn1 expfB ?a_gt1 // rootCK ?a_pos ?CratrE. 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