addIneq — Mathlib

Lean4
/-- If our goal is to add together two inequalities `t1 R1 0` and `t2 R2 0`,
`addIneq R1 R2` produces the strength of the inequality in the sum `R`,
along with the name of a lemma to apply in order to conclude `t1 + t2 R 0`.
-/
def addIneq : Ineq → Ineq → (Name × Ineq)
  | eq, eq => (``Linarith.eq_of_eq_of_eq, eq)
  | eq, le => (``Linarith.le_of_eq_of_le, le)
  | eq, lt => (``Linarith.lt_of_eq_of_lt, lt)
  | le, eq => (``Linarith.le_of_le_of_eq, le)
  | le, le => (``Linarith.add_nonpos, le)
  | le, lt => (``Linarith.add_lt_of_le_of_neg, lt)
  | lt, eq => (``Linarith.lt_of_lt_of_eq, lt)
  | lt, le => (``Linarith.add_lt_of_neg_of_le, lt)
  | lt, lt => (``Linarith.add_neg, lt)
Похожие утверждения