proposition: Lemma osum2_zero a b: ordinalp a -> ordinalp b -> a +o b = \0o -> (a = \0o /\ b = \0o).
proof: Proof. move=> oa ob s0; case: (ozero_dichot oa) => az. by rewrite -{2} s0 az (osum0l ob). by case: (proj2(olt_leT az (osum_Mle0 oa ob))). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)