placing a lemma about partial orders

Stream: new members

[Yakov Pechersky]

Where in mathlib would this go, if anywhere?

@[simp] lemma ne_iff_lt_iff_le {α : Type*} [partial_order α] {n m : α} : (n ≠ m ↔ n < m) ↔ n ≤ m :=
begin
  refine ⟨λ h, _, λ h, _⟩,
  { by_cases H : n = m,
    { exact le_of_eq H },
    { exact le_of_lt (h.mp H) } },
  { rcases eq_or_lt_of_le h with rfl|H,
    { simp [not_lt_of_ge] },
    { simp [H, ne_of_lt] } }
end

[Yakov Pechersky]

And why is not_lt_of_ge true for partial_order but le_of_not_gt needs linear_order?

[Mario Carneiro]

(1) Somewhere in algebra.order; (2) because le_of_not_gt has the form not A -> B, which is a disjunction A \/ B, and disjunctions like this usually only hold in the total order case

[Mario Carneiro]

The other direction A -> not B is closer to asymmetry, which has the form A -> B -> false and is true in any preorder

[Yakov Pechersky]

Gotcha. Issue was that \not k < k was not simplifying for a partial_order in a lemma that I have.

[Mario Carneiro]

that's lt_irrefl

[Yakov Pechersky]

Hmm why did I think that required linear_order? Must've gotten some wires crossed.

[Yakov Pechersky]

#5731