proposition: Lemma indecomp_prod2 a (b:= a *o omega0): \0o <o a -> [/\ indecomposable b, a <o b & forall c, indecomposable c -> a <o c -> b <=o c].
proof: Proof. move=> ap. have oa:= proj32_1 ap. have anz:= (nesym (proj2 ap)). have o1: \1o <o omega0 by apply /olt_omegaP; fprops. split; first by move /(indecomp_prodP o1 ap) : indecomp_omega. apply:(oprod_Meq1lt o1 ap). move=> c oic ac. move: (indecomp_div oic anz ac) => [z [oiz oz xp]]. rewrite /b xp; apply: (oprod_Mlele (oleR oa)). case: (indecomp_omega1 oiz) => // z1. move: xp; rewrite z1 oprod1r// => ca. by move: ac => [_]; rewrite ca. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)