proposition: Lemma ord_prime_prop2 a b c: \0o <o a -> \0o <o b -> osuccp b -> ordinalp c -> a *o b = oopow c -> a = oopow c /\ b = \1o.
proof: Proof. move => ap bp bs oc eq. have ob := proj32_1 bp; have ooc := (OS_pow OS_omega oc). move:(ovaluation_prod ap bp); rewrite eq (ovaluation_opow oc). case: (ozero_dichot (OS_valuation bp)) => vbz; last first. case (limit_nonsucc' (ovaluation3 bp vbz) bs). Ytac0; move => cva. move: (ovaluation6 ap) => [z sz av]. have oz: ordinalp z by case: sz => [t ot ->]; fprops. move: eq; rewrite av - cva - (oprodA ooc oz ob) => eq. move: (oprod2_simpl1 (OS_prod2 oz ob) (oopow_pos oc) eq) => eq1. by move: (oprod2_one oz ob eq1) => [-> b1]; rewrite (oprod1r ooc). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)