Ordered groups #
This file develops the basics of unbundled ordered groups.
Implementation details #
Unfortunately, the number of '
appended to lemmas in this file
may differ between the multiplicative and the additive version of a lemma.
The reason is that we did not want to change existing names in the library.
Alias of the reverse direction of sub_le_self_iff
.
Alias of the forward direction of neg_le_neg_iff
.
Alias of the reverse direction of sub_lt_self_iff
.
Alias of the forward direction of inv_lt'
.
Alias of Left.neg_le_self
.
Alias of Left.neg_lt_self
.
Alias of the forward direction of inv_lt_inv_iff
.
Alias of the forward direction of Left.inv_lt_one_iff
.
Uses left
co(ntra)variant.
Alias of Left.inv_lt_one_iff
.
Uses left
co(ntra)variant.
Alias of the forward direction of Left.one_lt_inv_iff
.
Uses left
co(ntra)variant.
Alias of the reverse direction of Left.one_lt_inv_iff
.
Uses left
co(ntra)variant.
Alias of the forward direction of le_inv_mul_iff_mul_le
.
Alias of the reverse direction of le_inv_mul_iff_mul_le
.
Alias of the reverse direction of inv_mul_le_iff_le_mul
.
Alias of the forward direction of lt_inv_mul_iff_mul_lt
.
Alias of the reverse direction of lt_inv_mul_iff_mul_lt
.
Alias of the reverse direction of inv_mul_lt_iff_lt_mul
.
Alias of the forward direction of inv_mul_lt_iff_lt_mul
.
Alias of the forward direction of inv_mul_lt_iff_lt_mul
.
Alias of the forward direction of inv_mul_lt_iff_lt_mul
.
Alias of the forward direction of sub_nonneg
.
Alias of the reverse direction of sub_nonneg
.
Alias of the reverse direction of sub_nonpos
.
Alias of the forward direction of sub_nonpos
.
Alias of the forward direction of le_sub_iff_add_le
.
Alias of the reverse direction of le_sub_iff_add_le
.
Alias of the reverse direction of le_sub_iff_add_le'
.
Alias of the forward direction of le_sub_iff_add_le'
.
Alias of the forward direction of sub_le_iff_le_add'
.
Alias of the reverse direction of sub_le_iff_le_add'
.
Alias of the reverse direction of sub_neg
.
For a - -b = a + b
, see sub_neg_eq_add
.
Alias of the forward direction of sub_neg
.
For a - -b = a + b
, see sub_neg_eq_add
.
Alias of sub_neg
.
For a - -b = a + b
, see sub_neg_eq_add
.
Alias of the forward direction of lt_sub_iff_add_lt
.
Alias of the reverse direction of lt_sub_iff_add_lt
.
Alias of the forward direction of sub_lt_iff_lt_add
.
Alias of the reverse direction of sub_lt_iff_lt_add
.
Alias of the reverse direction of lt_sub_iff_add_lt'
.
Alias of the forward direction of lt_sub_iff_add_lt'
.
Alias of the reverse direction of sub_lt_iff_lt_add'
.
Alias of the forward direction of sub_lt_iff_lt_add'
.