o ≠ 0 vs 0 < o

Stream: mathlib4

[Violeta Hernández]

Currently the ordinal API uses these two spellings somewhat interchangeably. Am I correct in saying we should prefer the former for statements and the latter for proofs?

[Violeta Hernández]

Converting h : 0 < o into o ≠ 0 is just h.ne'. Doing the converse requires Ordinal.pos_iff_ne_zero.2 h which is a hassle.

[Violeta Hernández]

Admittedly we should probably have an alias for that, but the point stands

[Yury G. Kudryashov]

We have docs#Ne.bot_lt but it gives a slightly wrong expression (which is defeq to what you need).

[Ruben Van de Velde]

Policy for Nat is ne for hypotheses and lt for conclusions

[Violeta Hernández]

Does that policy extend to inequalities? e.g. does something like b < c → a * b < a * c take 0 < a or a ≠ 0?

[Yury G. Kudryashov]

Probably, we should think again about this policy, since positivity doesn't care about 0 < a vs a ≠ 0.

[Kevin Buzzard]

It's also trivial to switch between the two so I wonder whether we should just choose a simp normal form.

[Yaël Dillies]

I don't think we should. a ≠ 0 is clearly algebraic, 0 < a is clearly order theoretic. Each has their use, and forcing people to use only one of them is friction