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
I now have to dictate the goal term, such as
apply (is_lim_seq_ext (fun n:nat => ...)), which is quite inefficient.
Last updated: Jan 28 2023 at 06:30 UTC