proposition: Lemma odiff_pr a b: a <=o b -> (ordinalp (b -o a) /\ b = a +o (b -o a)).
proof: Proof. move => ab;move: (ab) => [oa ob sab]; split; first exact: (OS_diff oa ob). move: b ob sab {ab}; apply: least_ordinal2' => d od H sad. rewrite (osum_rec_def oa (OS_diff oa od)); set_extens t; last first. case/setU2_P; [ apply: sad | by move /funI_P => [z /Zo_hi za ->]]. move => td; apply/setU2_P; case: (oleT_el oa (Os_ordinal od td)). move => [_ _ /(H _ td)] h. right; apply /funI_P. exists (t -o a) => //; apply:Zo_i; last by ue. exact:(ole_ltT_s od (odiff_Mle oa (Os_ordinal od td)) td). by move /(oltP oa); left. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)