proposition: Lemma indecomp_sier a b c: ordinalp a -> indecomposable c -> b <o c -> b +o a +o c = a +o c.
proof: Proof. move => oa ic lbc. have ob := proj31_1 lbc. have oc := (proj32_1 (proj1 ic)). case: (ozero_dichot ob)=> bp; first by rewrite bp (osum0l oa). move: (oquoremP oa bp); set q := oquo _ _; set r := orem _ _. move=>[oq or dv rs]. case: (oleT_el OS_omega oq) => lt1. move: (oleT (oprod_Meqle lt1 ob) (osum_Mle0 (OS_prod2 ob oq) or)). by rewrite - dv; move/(ord_negl_alt ob oa) => ->. have H := (OS_prod2 ob oq). rewrite - (osumA ob oa oc) dv - (osumA H or oc). rewrite (indecomp_prop1 ic (olt_ltT rs lbc))(osumA ob H oc)(oprod2_nsucc ob oq). have ->: \1o +o q = osucc q. move/(oltP OS_omega): lt1 => qN. rewrite - (succ_of_nat qN) (Nsucc_rw qN). by rewrite (osum2_2int NS1 qN) csumC. by rewrite (oprod2_succ ob oq) - (osumA H ob oc) (indecomp_prop1 ic lbc). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)