proposition: Lemma osum0l a: ordinalp a -> \0o +o a = a.
proof: Proof. move: a; apply: least_ordinal2' => c oc prc. rewrite (osum_rec_def OS0 oc) set0_U2; set_extens t. by move => /funI_P [z zc ->]; rewrite prc. by move => tc; apply/funI_P; ex_tac; rewrite prc. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)