proposition: Lemma telescope_prodf_eq n m (f u : nat -> F) : (forall k, n < k < m -> f k != 0) -> n < m -> (forall k, n <= k < m -> u k = f k.+1 / f k) -> \prod_(n <= k < m) u k = f m / f n.
proof: Proof. by move=> ? ? uE; under eq_big_nat do rewrite uE //=; exact: telescope_prodf. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop prime binomial)