proposition: Lemma ointv_pr1 b: ordinalp b -> ordinal_interval \0o b = b.
proof: Proof. move=> ob; set_extens t. by move /(ointvP0 ob) /oltP0 => [ _ _]. by move => tb; move:(Os_ordinal ob tb) => ot;apply /(ointvP0 ob) /oltP0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)