mathlib documentation

tactic.omega.int.dnf

DNF transformation #

@[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.int.le_and_le_iff_eq {α : Type} [partial_order α] {a b : α} :
a b b a a = b