proposition: Lemma oprod_succP a b: ordinalp a -> ordinalp b -> (osuccp (a *o b) <-> osuccp a /\ osuccp b).
proof: Proof. move => oa ob. split; last first. move => [osa [c oc ->]]; rewrite (oprod2_succ oa oc). by apply/(osum_succP (OS_prod2 oa oc) oa); right. move => [c oc h]. case: (ordinal_limA oa). - by move => az; move: h; rewrite az oprod0l // => /esym /osucc_nz. - move => sa; split => //. have ap: \0o <o a by move: sa => [a' /olt0S oa' ->]. case: (ordinal_limA ob). + by move => bz; move: h; rewrite bz oprod0r // => /esym /osucc_nz. + done. + move => lb; move: (oprod_limit ap lb); rewrite h. by move/limit_ordinal_P => [ra rb]; case /oltSSP:(rb _ (oltS oc)). - move => /limit_ordinal_P [ap la]. move: (oquoremP oc ap) => [oq or cv rs]. move:(osumA (OS_prod2 oa oq) or OS1). rewrite - cv (osucc_pr or) (osucc_pr oc) => ha. move: (OS_succ oc) (OS_succ or)(la _ rs) => osc osr rs'. have d1:odiv_pr0 (osucc c) a (oquo c a) (osucc (orem c a)) by []. have d2: odiv_pr0 (osucc c) a b \0o. by split; fprops; rewrite (osum0r (OS_prod2 oa ob)) h. case:(osucc_nz (proj2(odivision_unique osc oa d1 d2))). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)