mathlib documentation

tactic.omega.nat.neg_elim

@[simp]

push_neg p returns the result of normalizing ¬ p by pushing the outermost negation all the way down, until it reaches either a negation or an atom

Equations
theorem omega.nat.le_and_le_iff_eq {α : Type} [partial_order α] {a b : α} :
a b b a a = b