proposition: Lemma telescope_prod_nat (a b : nat) (f : nat -> R) : (forall k, (a <= k < b)%N -> f k != 0) -> (a < b)%N -> \prod_(a <= k < b) (f (k + 1)%N / f k) = f b / f a.
proof: Proof. case: b => // b hf; rewrite ltnS => leab. rewrite big_split prodfV big_nat_recr //= addn1 [_ * f b.+1]mulrC. rewrite big_nat_recl //= invfM mulrACA -[RHS]mulr1; congr (_ * _). rewrite -prodfV -big_split big_nat_cond big1 => //= i /andP[/andP[leai ltib] _]. by rewrite addn1 divff ?hf // ltnS ltib leqW. Qed.
imports: mathcomp(all_ssreflect all_algebra all_field) mathcomp(bigenough)