Commit 2022-11-17 03:31 1049885d

View on Github →

feat: positivity tactic (#578)

  • depends on #574 Implements the positivity tactic core, plus several of the positivity extensions. Most of the remaining extensions are blocked on theory files.

Estimated changes

added theorem add_nonneg
added theorem add_pos
added theorem lt_add_of_le_of_pos
added theorem lt_add_of_pos_of_le
added theorem mul_ne_zero
added theorem mul_nonneg
added theorem mul_pos
added theorem pow_bit0_nonneg
added theorem pow_ne_zero
added theorem pow_nonneg
added theorem pow_pos
added theorem pow_zero_pos
added theorem ne_of_ne_of_eq'
added theorem zero_le