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 13 2024 at 01:02 UTC