proposition: Lemma oone_dichot x y: x <o y -> (y = \1o \/ \1o <o y).
proof: Proof. move => h; case: (equal_or_not y \1o) => h'; [by left | right; split; fprops]. apply: oge1; [exact : (proj32_1 h) | move=> h''; case: (@olt0 x); ue]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)