feat(data/sign): `left.sign_neg`, `right.sign_neg` (#15652)
Add lemmas that the sign of `-a` is the negation of the sign of `a`,
for two kinds of ordered additive groups (corresponding to the type
classes on the `left` and `right` variants of the `neg_pos_iff` and
`neg_neg_iff` lemmas used).
