Stream: Coq users

Topic: Rewriting Limit


view this post on Zulip Yosuke Ito (May 31 2021 at 12:31):

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: Jan 28 2023 at 06:30 UTC