proposition: Lemma osum2_simpl a b c: ordinalp a -> ordinalp b -> ordinalp c -> c +o a = c +o b -> a = b.
proof: Proof. move=> oa ob oc so. by case: (oleT_ell oa ob) => h //; move: (osum_Meqlt h oc); rewrite so; move=> [_]; case. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)