Commit 2024-02-06 21:44 8cc0b2a6

feat(Positivity): Strictness extractors (#10274) Define combinators to turn strictness assumptions into proofs of nonnegativity or nonzeroness. These are useful to write positivity extensions where having 0 < a doesn't help. We might want binary combinators in the future. Eg the pattern "Binary function foo is positive/nonnegative/nonzero if its inputs are" is very common.