proposition: Lemma ointvP b: ordinalp b -> forall a z, (inc z (ordinal_interval a b) <-> (a <=o z /\ z <o b)).
proof: Proof. move => ob a z; split. by move => /Zo_P [zb ab]; move:(proj32 ab) => oz;split => //; apply /oltP0. by move => [az] /oltP0 [pa pb pc]; apply: Zo_i. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)