Ordered subfields

Stream: Is there code for X?

[Artie Khovanov]

Let $K$ be an ordered field, and $L/K$ a field extension ($L$ not necessarily ordered). I can't find anything about the ordered intermediate extensions of $K$, as terms of a type such as IntermediateField (probably we want a fresh type). What I need is the "ordered extension" relation and existence of directed unions under this relation. Is there anything at all in this direction?

[Filippo A. E. Nuccio]

There is a "similar" result for nonarchimedean norms in docs#exists_nonarchimedean_pow_mul_seminorm_of_finiteDimensional

[Artie Khovanov]

Extension of nonarchimedean norms has some mathematical content, whereas (I think) what I'm looking for is mathematically trivial?