Commit 2024-11-11 10:06 634add1e

View on Github →

feat(Data/Nat/Nth): count_nth_succ_of_infinite (#18835) Add a lemma count_nth_succ_of_infinite, which is to count_nth_succ as count_nth_of_infinite is to count_nth.

Estimated changes