proposition: Lemma odiff_pr1 a b: ordinalp a -> ordinalp b -> (a +o b) -o a = b.
proof: Proof. move=> oa ob. have [so sp] := (odiff_pr (osum_Mle0 oa ob)). by move: (osum2_simpl ob so oa sp). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)