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: Oct 03 2023 at 04:02 UTC