Dear Coq users,

If I were to rewrite the term in `\big[op/idx]`

, I can use `under eq_big_nat`

tactic. But is there any way to rewrite the term in `is_lim_seq`

(in Coquelicot) like `under`

?

I now have to dictate the goal term, such as `apply (is_lim_seq_ext (fun n:nat => ...))`

, which is quite inefficient.

Last updated: Jun 20 2024 at 12:02 UTC