[Merged by Bors] - chore: avoid superfluous use of push_neg with contrapose, by_contra o…#37937

grunweg wants to merge 2 commits intoleanprover-community:masterleanprover-community/mathlib4:masterfrom

grunweg:less-neggrunweg/mathlib4:less-negCopy head branch name to clipboard