proposition: Lemma ord2_trichotomy a: ordinalp a -> [\/ a = \0o, a = \1o | \2o <=o a].
proof: Proof. move=> oa. case: (equal_or_not a \0o); first by constructor 1. case: (equal_or_not \1o a); first by constructor 2. by move => a1 a0; constructor 3; apply /oge2P; split =>//; apply: oge1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)