proposition: Lemma indecomp_div x y: indecomposable x -> y <> \0o -> y <o x -> exists z, [/\ indecomposable z, ordinalp z & x = y *o z].
proof: Proof. move=> oix ynz ltyx. move: (ltyx) => [[oy ox _] _]. have yp:= (ord_ne0_pos oy ynz). move: (oquoremP ox yp) => [oq or /esym xeq [lt1 _]]. move:(proj2(ole_ltT lt1 ltyx)) => xnr. case: (ozero_dichot oq) => qz. by move: xnr; rewrite -{2} xeq qz oprod0r (osum0l or). case: (indecomp_pr (OS_prod2 oy oq) or oix xeq) => ea //. exists (oquo x y); split => //. case: (oone_dichot qz) => q1; first by rewrite q1; apply: indecomp_one. apply/(indecomp_prodP q1 yp); ue. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)