Theoremsle_add_self, le_self_add, toAddLeftMono, toExistsAddOfLE, toIsOrderedAddMonoid, le_mul_self, le_self_mul, toExistsMulOfLE, toIsOrderedMonoid, toMulLeftMono, one_lt, pos, one_lt, pos, of_ge, of_gt, of_gt', pos, add_pos_iff, bot_eq_one, bot_eq_one', bot_eq_zero, bot_eq_zero', eq_one_or_one_lt, eq_zero_or_pos, exists_one_lt_mul_of_lt, exists_pos_add_of_lt, isBot_one, isBot_zero, le_add_left, le_add_of_le_left, le_add_of_le_right, le_add_right, le_add_self, le_iff_exists_add, le_iff_exists_add', le_iff_exists_mul, le_iff_exists_mul', le_mul_left, le_mul_of_le_left, le_mul_of_le_right, le_mul_right, le_mul_self, le_of_add_le_left, le_of_add_le_right, le_of_mul_le_left, le_of_mul_le_right, le_one_iff_eq_one, le_self_add, le_self_mul, lt_iff_exists_add, lt_iff_exists_mul, min_add_distrib, min_add_distrib', min_mul_distrib, min_mul_distrib', min_one, min_zero, nonpos_iff_eq_zero, not_lt_one, not_lt_zero, not_neg, one_le, one_lt_iff_ne_one, one_lt_mul_iff, one_lt_of_gt, one_lt_of_ne_one, one_min, one_notMem_iff, pos_iff_ne_zero, pos_of_gt, pos_of_ne_zero, self_le_add_left, self_le_add_right, self_le_mul_left, self_le_mul_right, zero_le, zero_min, zero_notMem_iff | 79 |