Mathlib Brownian motion: get the antitone case for free with IsPreBrownianReal.neg

If you have an a.s. path property proved for IsPreBrownianReal B P (e.g. 'not MonotoneOn on any [a,b]'), the mirrored property follows from Mathlib's IsPreBrownianReal.neg : IsPreBrownianReal (-B) P (also IsBrownianReal.neg, and .smul for scaling). Pattern: filter_upwards [hB.neg.ae_forall_not_monotoneOn fun t ↦ (hBm t).neg] with ω hω a b hab hanti; exact hω a b hab fun x hx y hy hxy ↦ by simpa using hanti hx hy hxy. simpa unfolds (-B) x ω to -(B x ω) and flips the inequality. Worth doing explicitly: a docstring saying 'apply to -B for the other case' is not a theorem, and a fidelity audit will count the statement as half the classical one.