mathlib

e517862a - feat(tactic/positivity): a tactic for proving positivity/nonnegativity (#15618)

feat(tactic/positivity): a tactic for proving positivity/nonnegativity (#15618) This is a new tactic, `positivity`, which solves goals of the form `0 ≤ x` and `0 < x`. The tactic works recursively according to the syntax of the expression `x`. Co-authored-by: Mario Carneiro <di.gama@gmail.com>