Commit 2022-09-30 00:01 4ed50443
View on Github →feat(tactic/positivity): Extension for finset.card (#16637)
A best effort positivity extension for finset.card. This looks for an assumption of the form s.nonempty in context to prove 0 < s.card.