proposition: Lemma OS_diff a b: ordinalp a -> ordinalp b -> ordinalp (b -o a).
proof: Proof. move => oa ob. apply: ordinal_pr; last by move => t /Zo_S /(Os_ordinal ob). move => u /Zo_P [ub /(oltP ob) ss] t tu. apply: (Zo_i (ordinal_transitive ob ub tu)). apply /(oltP ob); apply: ole_ltT ss; apply:osum_Meqle => //. by move/(oltP (Os_ordinal ob ub)): tu => []. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)