proposition: Lemma Exercise6_12e p: posnatp p -> p *o (osucc omega0) = (omega0 +o p).
proof: Proof. move/posnat_ordinalp => [np no]; move: (proj31_1 no) => on. have h := (oprod_int_omega no np). by rewrite -(osucc_pr OS_omega)(oprodD OS_omega OS1 on) h (oprod1r on). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)