`m+[n∸m]≡n` in the wrong section

[gallais]

m+[n∸m]≡n : m ≤ n → m + (n ∸ m) ≡ n

is under the header "Properties of ∸ and +" but does not mention _+_.

[Taneb]

...yes it does?

[gallais]

lmao. Too tired by all this marking.