mathlib3

feat(data/nat/basic): b = c if b - a = c - a (assuming a ≤ b and a ≤ c)

#862

Merged