proposition: Lemma oadd1_fix a: ordinalp a -> (\1o +o a = a <-> omega0 <=o a).
proof: Proof. move => ox; split; last by apply:osum_1inf. move => h; case: (oleT_el OS_omega ox) => // /olt_omegaP xN. move: (osum2_2int NS1 xN); rewrite h csumC - (Nsucc_rw xN). by move: xN => /NatP /finite_cP [_]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)