proposition: Lemma oleP a: ordinalp a -> forall x, (x <=o a <-> inc x (osucc a)).
proof: Proof. move=> oa x; split. by move=> [pa _ pc]; apply /ordinal_sub4P. move => aux; move: (ordinal_sub3 oa aux) => xa; split => //. apply: (Os_ordinal (OS_succ oa) aux). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)