I don't know if there is a standard term for this, but by "negative trichotomy" I mean ¬ (¬ 𝐴 < 𝐵 ∧ ¬ 𝐴 = 𝐵 ∧ ¬ 𝐵 < 𝐴). This holds for constructive real numbers as an easy consequence of 𝐴 ≤ 𝐵 ↔ ¬ 𝐵 < 𝐴 and 𝐴 = 𝐵 ↔ (𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐴) but the ordinal analogue to the former is 𝐴 ⊆ 𝐵 ↔ ¬ 𝐵 ∈ 𝐴 and I only am aware of a proof of that for the special case of the natural numbers.
One possible literature reference is https://www.cs.bham.ac.uk/~mhe/TypeTopology/Ordinals.Notions.html#is-decidable-order but I don't read agda in general, or TypeTopology in particular, well enough to know whether that is relevant or not.
At the risk of stating the obvious, ¬ (¬ 𝐴 < 𝐵 ∧ ¬ 𝐴 = 𝐵 ∧ ¬ 𝐵 < 𝐴) is equivalent to ¬ ¬ ( 𝐴 < 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 < 𝐴) in intuitionistic logic, so the problem can be stated either way.