proposition: Lemma telescope_prod_int (a b : int) (f : int -> R) : (forall k, a <= k < b -> f k != 0) -> a < b -> \prod_(a <= k < b :> int) (f (k + 1) / f k) = f b / f a.
proof: Proof. move=> hf; rewrite -{2}[a]add0r big_addz => hab /=. case e: (b - a) => [bma | bma]; last by move: hab; rewrite -subr_gt0 e. rewrite eq_big_int_nat /=. transitivity (\prod_(0 <= i < bma) (f (Posz (i + 1)%N + a) / f (Posz i + a))). apply: congr_big_nat => // i _ ; by rewrite PoszD addrAC. rewrite (@telescope_prod_nat _ _ _ (fun i => f (Posz i + a))%R) //. - by rewrite add0r -e addrNK. - move=> k /andP [h0k hbma]; apply: hf; rewrite lerDr -ltrBrDr e. by rewrite lez_nat ltz_nat h0k /=. - have : 0 < b - a by rewrite subr_gt0. by rewrite e ltz_nat. Qed.
imports: mathcomp(all_ssreflect all_algebra) extra_mathcomp