add_min_max

Stream: Is there code for X?

[Xavier Xarles]

I am quite sure this is already in mathlib, but I cannot find it

import data.int.basic
lemma add_min_max {a b : ℕ}: a+b= (min a b)+(max a b):=
begin
  cases le_total a b with h h,
  rw [min_eq_left h,max_eq_right h],
  rw [min_eq_right h,max_eq_left h,add_comm a b],
end

Of course it can be done with other type of numbers or much more generally...

Thanks!

[Yaël Dillies]

docs#min_add_max

[Kevin Buzzard]

import tactic
lemma add_min_max {a b : ℕ}: a+b= (min a b)+(max a b):=
begin
  library_search
end

is the way to answer questions like this. Note that "equality is not symmetric" in Lean! In the maths library the convention is to put the more complicated expression on the left hand side of the equality (so that you can rw more easily) , so you would expect the result to be min a b + max a b = a + b, as indeed it is, but library_search is smart enough to spot the result anyway.

[Xavier Xarles]

I tried library_search but didn't work. May be because I did not import tactic first?

[Kevin Buzzard]

import data.int.basic
lemma add_min_max {a b : ℕ}: a+b= (min a b)+(max a b):=
begin
  library_search
end

works for me. I often import tactic though because it just guarantees that you have a bunch of basic stuff imported.