| Metric | Count |
|---|
| Definitions | 0 |
TheoremstoOrderedSub, inv, neg, inv, neg, inv_le_one_iff, inv_le_self, inv_lt_one_iff, inv_lt_self, neg_le_self, neg_lt_self, neg_neg_iff, neg_nonpos_iff, neg_pos_iff, nonneg_neg_iff, one_le_inv_iff, one_lt_inv_iff, self_le_inv, self_le_neg, self_lt_inv, self_lt_neg, inv, neg, inv, neg, inv_le_one_iff, inv_le_self, inv_lt_one_iff, inv_lt_self, neg_le_self, neg_lt_self, neg_neg_iff, neg_nonpos_iff, neg_pos_iff, nonneg_neg_iff, one_le_inv_iff, one_lt_inv_iff, self_le_inv, self_le_neg, self_lt_inv, self_lt_neg, inv, neg, inv, neg, inv, neg, inv, neg, add_le_of_le_neg_add, add_le_of_le_sub_left, add_le_of_le_sub_right, add_lt_of_lt_neg_add, add_lt_of_lt_sub_left, add_lt_of_lt_sub_right, add_neg_le_add_neg_iff, add_neg_le_iff_le_add, add_neg_le_iff_le_add', add_neg_le_neg_add_iff, add_neg_lt_add_neg_iff, add_neg_lt_iff_le_add', add_neg_lt_iff_lt_add, add_neg_lt_neg_add_iff, add_neg_neg_iff, add_neg_nonpos_iff, add_neg_nonpos_iff_le, cmp_div_one', cmp_sub_zero, div_le_comm, div_le_div'', div_le_div_flip, div_le_div_iff', div_le_div_iff_left, div_le_div_iff_right, div_le_div_left', div_le_div_right', div_le_iff_le_mul, div_le_iff_le_mul', div_le_inv_mul_iff, div_le_one', div_le_self_iff, div_lt_comm, div_lt_div'', div_lt_div_iff', div_lt_div_iff_left, div_lt_div_iff_right, div_lt_div_left', div_lt_div_right', div_lt_iff_lt_mul, div_lt_iff_lt_mul', div_lt_one', div_lt_self_iff, inv_le_div_iff_le_mul, inv_le_div_iff_le_mul', inv_le_iff_one_le_mul, inv_le_iff_one_le_mul', inv_le_inv_iff, inv_le_one', inv_lt', inv_lt_div_iff_lt_mul, inv_lt_div_iff_lt_mul', inv_lt_iff_one_lt_mul, inv_lt_iff_one_lt_mul', inv_lt_inv_iff, inv_lt_of_inv_lt', inv_lt_one', inv_lt_one_iff_one_lt, inv_mul_le_iff_le_mul, inv_mul_le_iff_le_mul', inv_mul_le_of_le_mul, inv_mul_le_one_iff, inv_mul_lt_iff_lt_mul, inv_mul_lt_iff_lt_mul', inv_mul_lt_of_lt_mul, inv_mul_lt_one_iff, inv_mul_lt_one_iff_lt, inv_of_one_lt_inv, le_add_neg_iff_add_le, le_add_neg_iff_le, le_add_of_sub_left_le, le_div_comm, le_div_iff_mul_le, le_div_iff_mul_le', le_div_self_iff, le_iff_forall_one_lt_lt_mul, le_iff_forall_pos_lt_add, le_inv_iff_mul_le_one_left, le_inv_iff_mul_le_one_right, le_inv_mul_iff_le, le_inv_mul_iff_mul_le, le_inv_mul_of_mul_le, le_mul_inv_iff_le, le_mul_inv_iff_mul_le, le_neg_add_iff_add_le, le_neg_add_iff_le, le_neg_add_of_add_le, le_neg_iff_add_nonpos_left, le_neg_iff_add_nonpos_right, le_of_forall_one_lt_lt_mul, le_of_forall_pos_lt_add, le_of_neg_le_neg, le_of_sub_nonneg, le_of_sub_nonpos, le_one_of_one_le_inv, le_sub_comm, le_sub_iff_add_le, le_sub_iff_add_le', le_sub_left_of_add_le, le_sub_right_of_add_le, le_sub_self_iff, lt_add_neg_iff_add_lt, lt_add_neg_iff_lt, lt_add_of_neg_add_lt, lt_add_of_neg_add_lt_left, lt_add_of_sub_left_lt, lt_add_of_sub_right_lt, lt_div_comm, lt_div_iff_mul_lt, lt_div_iff_mul_lt', lt_inv', lt_inv_iff_mul_lt_one, lt_inv_iff_mul_lt_one', lt_inv_mul_iff_lt, lt_inv_mul_iff_mul_lt, lt_inv_mul_of_mul_lt, lt_inv_of_lt_inv, lt_mul_inv_iff_lt, lt_mul_inv_iff_mul_lt, lt_mul_of_inv_mul_lt, lt_mul_of_inv_mul_lt_left, lt_neg, lt_neg_add_iff_add_lt, lt_neg_add_iff_lt, lt_neg_add_of_add_lt, lt_neg_iff_add_neg, lt_neg_iff_add_neg', lt_neg_of_lt_neg, lt_of_inv_lt_inv, lt_of_neg_lt_neg, lt_of_sub_neg, lt_of_sub_pos, lt_or_lt_of_div_lt_div, lt_or_lt_of_sub_lt_sub, lt_sub_comm, lt_sub_iff_add_lt, lt_sub_iff_add_lt', lt_sub_left_of_add_lt, lt_sub_right_of_add_lt, mul_inv_le_iff_le_mul, mul_inv_le_iff_le_mul', mul_inv_le_inv_mul_iff, mul_inv_le_mul_inv_iff', mul_inv_le_one_iff, mul_inv_le_one_iff_le, mul_inv_lt_iff_le_mul', mul_inv_lt_iff_lt_mul, mul_inv_lt_inv_mul_iff, mul_inv_lt_mul_inv_iff', mul_inv_lt_one_iff, mul_le_of_le_inv_mul, mul_lt_of_lt_inv_mul, neg_add_le_iff_le_add, neg_add_le_iff_le_add', neg_add_le_of_le_add, neg_add_lt_iff_lt_add, neg_add_lt_iff_lt_add', neg_add_lt_of_lt_add, neg_add_neg_iff, neg_add_neg_iff_lt, neg_add_nonpos_iff, neg_le_iff_add_nonneg, neg_le_iff_add_nonneg', neg_le_neg_iff, neg_le_self, neg_le_sub_iff_le_add, neg_le_sub_iff_le_add', neg_lt, neg_lt_iff_pos_add, neg_lt_iff_pos_add', neg_lt_neg_iff, neg_lt_of_neg_lt, neg_lt_self, neg_lt_sub_iff_lt_add, neg_lt_sub_iff_lt_add', neg_lt_zero, neg_neg_iff_pos, neg_nonneg, neg_nonpos, neg_of_neg_pos, neg_pos, neg_pos_of_neg, nonneg_of_neg_nonpos, nonpos_of_neg_nonneg, one_le_div', one_le_inv', one_le_of_inv_le_one, one_lt_div', one_lt_inv', one_lt_inv_of_inv, one_lt_of_inv_lt_one, pos_of_neg_neg, sub_le_comm, sub_le_iff_le_add, sub_le_iff_le_add', sub_le_neg_add_iff, sub_le_self, sub_le_self_iff, sub_le_sub, sub_le_sub_flip, sub_le_sub_iff, sub_le_sub_iff_left, sub_le_sub_iff_right, sub_le_sub_left, sub_le_sub_right, sub_left_le_of_le_add, sub_left_lt_of_lt_add, sub_lt_comm, sub_lt_iff_lt_add, sub_lt_iff_lt_add', sub_lt_self, sub_lt_self_iff, sub_lt_sub, sub_lt_sub_iff, sub_lt_sub_iff_left, sub_lt_sub_iff_right, sub_lt_sub_left, sub_lt_sub_right, sub_lt_zero, sub_neg, sub_neg_of_lt, sub_nonneg, sub_nonneg_of_le, sub_nonpos, sub_nonpos_of_le, sub_pos, sub_pos_of_lt, sub_right_lt_of_lt_add | 277 |
| Total | 277 |