proposition: Lemma ordinal_sub4P x y: ordinalp x -> ordinalp y -> (sub x y <-> inc x (osucc y)).
proof: Proof. move=> ox oy; split; last by apply: ordinal_sub3. by case /(ordinal_sub ox oy) => H; apply/setU1_P; [right | left]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)