proposition: Lemma ordinal_sub2 x y: ordinalp y -> inc x y -> ssub x y.
proof: Proof. move=> /ordinal_trans_dec [ty dy xy]; split; first by apply: ty. by move => ac; case: (dy _ xy); rewrite {2} ac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)