proposition: Lemma odiff_pr2 a b c: ordinalp a -> ordinalp b -> ordinalp c -> (a +o c = b) -> c = b -o a.
proof: Proof. move => oa ob oc h. have lab: a<=o b by rewrite -h; exact :(osum_Mle0 oa oc). have [pa pb]:= (odiff_pr lab). rewrite pb in h; exact: (osum2_simpl oc pa oa h). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)