proposition: Lemma telescope_nat (a b : nat) (f : nat -> R) : (a <= b)%N -> \sum_(a <= k < b) (f (k + 1)%N - f k) = f b - f a.
proof: Proof. rewrite leq_eqVlt => /predU1P[->|]; first by rewrite big_geq // subrr. case: b => // b; rewrite ltnS => leab. rewrite big_split sumrN big_nat_recr //= addn1 [_ + f _]addrC big_nat_recl //=. rewrite opprD addrACA -[RHS]addr0; congr (_ + _). by rewrite -sumrN -big_split big1 => //= i _; rewrite addn1 subrr. Qed.
imports: mathcomp(all_ssreflect all_algebra all_field) mathcomp(bigenough)