Lemmas for linarith
#
This file contains auxiliary lemmas that linarith
uses to construct proofs.
If you find yourself looking for a theorem here, you might be in the wrong place.
theorem
linarith.eq_of_eq_of_eq
{α : Type u_1}
[ordered_semiring α]
{a b : α}
(ha : a = 0)
(hb : b = 0) :
theorem
linarith.le_of_eq_of_le
{α : Type u_1}
[ordered_semiring α]
{a b : α}
(ha : a = 0)
(hb : b ≤ 0) :
theorem
linarith.lt_of_eq_of_lt
{α : Type u_1}
[ordered_semiring α]
{a b : α}
(ha : a = 0)
(hb : b < 0) :
theorem
linarith.le_of_le_of_eq
{α : Type u_1}
[ordered_semiring α]
{a b : α}
(ha : a ≤ 0)
(hb : b = 0) :
theorem
linarith.lt_of_lt_of_eq
{α : Type u_1}
[ordered_semiring α]
{a b : α}
(ha : a < 0)
(hb : b = 0) :
@[nolint]
theorem
linarith.eq_of_not_lt_of_not_gt
{α : Type u_1}
[linear_order α]
(a b : α)
(h1 : ¬a < b)
(h2 : ¬b < a) :
a = b