proposition: Lemma indecomp_prod3 a: \0o <o a -> (osucc a) *o omega0 = a *o omega0.
proof: Proof. move=> ap. have oa:= (proj32_1 ap). move: (olt0S oa) => sp. move: (indecomp_prod2 ap) (indecomp_prod2 sp). set (x := (osucc a) *o omega0); set (y:= a *o omega0). move => [p1 p2 p3] [q1 q2 q3]. apply: oleA; last by apply: (p3 _ q1);apply /oleSltP;move: q2=> [ok _]. apply: (q3 _ p1); split; first by apply /oleSltP. by move=> h; move: (indecomp_example ap);rewrite h. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)