proposition: Lemma osum2_succ x y: ordinalp x -> ordinalp y -> osucc (x +o y) = x +o (osucc y).
proof: Proof. move=> oa ob. rewrite -(osucc_pr ob) (osumA oa ob OS1) osucc_pr ;fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)