proposition: Lemma ord2_trichotomy1 a: \2o <=o a -> (a <> \0o /\ a <> \1o).
proof: Proof. move=> h; split; first exact: (nesym (proj2 (olt_leT olt_02 h))). exact: (nesym (proj2 (olt_leT olt_12 h))). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)