proposition: Lemma indecomp_prodP x y: \1o <o x -> \0o <o y -> (indecomposable x <-> indecomposable (y *o x)).
proof: Proof. move=> cx1 cy0. move: (proj32_1 cx1) (proj32_1 cy0) => ox oy. move: (olt_leT olt_01 (proj1 cx1)) => xp. split; last first. move=> [ha hb]; split => //; move=> a b ax bx. move: (oprod_Meqlt ax cy0) => lt1. move: (oprod_Meqlt bx cy0) => lt2. move: (proj31_1 ax) (proj31_1 bx) => oa ob. move: (hb _ _ lt1 lt2); rewrite - oprodD //. by move=> h1; dneg h2;rewrite h2. move=> xi. move: (OS_prod2 oy ox) OS1 => op io1. have xynz: \0o <o y *o x by apply: oprod2_pos. apply/(indecompP xynz) => z ltz. have oz: ordinalp z by move: ltz => [[oz _]_]. move: (odivision_exists oy ox ltz)=> [[oq or zv ltrq] ltry]. apply: oleA; last by apply: osum_M0le. rewrite - {2} (indecomp_prop1 xi ltry) -{2} (indecomp_prop1 xi cx1) osumA //. rewrite (oprodD (OS_sum2 oq OS1) ox oy) {1} zv (oprodD oq OS1 oy). apply:(osum_Mleeq _ (proj32_1 xynz)); apply:(osum_Meqle _ (OS_prod2 oy oq)). rewrite (oprod1r oy); exact: (proj1 ltrq). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)