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