proposition: Lemma ointvP0 b: ordinalp b -> forall z, (inc z (ordinal_interval \0o b) <-> z <o b).
proof: Proof. move=> bb z; apply: (iff_trans (ointvP bb _ _ )). split; first by case. move=> h; split => //; exact: (ole0x (proj31_1 h)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)