proposition: Lemma ord_prime_prop3 a b c (d := odegree a): \0o <o a -> limit_ordinal b -> ordinalp c -> a *o b = oopow c -> d <=o c /\ b = oopow (c -o d).
proof: Proof. move => ap limb oc eq. move:(proj32_1 ap)(proj31 limb) => oa ob. move:(OS_degree oa) (OS_degree ob) => oda odb. move: (odegree_prod ap (limit_pos limb)). rewrite eq -/d (odegree_opow oc) => eq1. split; first by rewrite eq1; apply:(osum_Mle0 oda odb). move: eq; rewrite /oopow (CNF_prod_pr3 ap limb) -/d eq1. rewrite (opow_sum OS_omega oda odb) (odiff_pr1 oda odb). by move/(oprod2_simpl ob (OS_pow OS_omega odb) (oopow_pos oda)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)