proposition: Lemma ointv1 b: ordinalp b -> forall a, inc a (ordinal_interval \1o b) <-> (\0o <o a /\ a <o b).
proof: Proof. move => ob a; split. by move /(ointvP ob) => [/oge1P wp1 wp2]. by move => [/oge1P wp1 wp2]; apply /(ointvP ob). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)