proposition: Lemma telescope_prodr n m (f : nat -> R) : (forall k, n < k < m -> f k \is a unit) -> n < m -> \prod_(n <= k < m) (f k / f k.+1) = f n / f m.
proof: Proof. move=> Uf ltnm; rewrite (telescope_big (fun i j => f i / f j)) ?ltnm//. by move=> k ltnkm /=; rewrite mulrA divrK// Uf. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop prime binomial)