Commit 2023-04-19 07:15 df4f506d

View on Github →

chore: fix push_neg on > (#3518)

Estimated changes

Modified Mathlib/Tactic/PushNeg.lean

added theorem Mathlib.Tactic.PushNeg.not_ge_eq

added theorem Mathlib.Tactic.PushNeg.not_gt_eq

Modified test/push_neg.lean