a + b - c = a - c + b

Stream: Is there code for X?

[Eric Wieser]

library_search is being slow for me. Do we have the versions of these lemmas using subtraction?

import algebra.group.basic

example {A} [add_comm_monoid A] (a b c : A) : a + b + c = a + c + b := add_right_comm _ _ _
example {A} [add_comm_group A] (a b c : A) : a + b - c = a - c + b := by library_search

example {A} [add_comm_monoid A] (a b c : A) : a + (b + c) = b + (a + c) := add_left_comm _ _ _
example {A} [add_comm_group A] (a b c : A) : a + (b - c) = b + (a - c) := by library_search

[Eric Wieser]

Ah, it finished - we have the first as (sub_add_eq_add_sub a c b).symm, it can't find the second

[Eric Wieser]

Do add_sub_right_comm and add_sub_left_comm make sense as more discoverable names for these?