Positivity extensions for finsets

This file provides a few positivity extensions that cannot be in either the finset files (because they don't know about ordered fields) or in Tactic.Positivity.Basic (because it doesn't want to know about finiteness).

def Mathlib.Meta.Positivity.evalFinsetCard : Mathlib.Meta.Positivity.PositivityExt

Extension for Finset.card. s.card is positive if s is nonempty.

It calls Mathlib.Meta.proveFinsetNonempty to attempt proving that the finset is nonempty.

def Mathlib.Meta.Positivity.evalFintypeCard : Mathlib.Meta.Positivity.PositivityExt

Extension for Fintype.card. Fintype.card α is positive if α is nonempty.