proposition: Lemma least_rem_p6 x c: \0o <o x -> is_rem_of x c -> indecomposable c -> c = (least_rem x).
proof: Proof. move => cp; move: c. pose p y := \0o <o y -> forall c, is_rem_of y c -> indecomposable c -> c = least_rem y. move: (proj32_1 cp) => ox; move: cp. case:(least_ordinal6 p ox) => //; set y := least_ordinal _ _. move => [oy yleast]; case => yp. move:(CNFr_exists_aux yp) =>[n [r [on lry _ yv2]]]. have oon := (OS_oopow on). have or := (proj31_1 lry). move: (indecomp_prop4 on) => iT. case: (ozero_dichot or) => rz. move: yv2 iT; rewrite rz (osum0r oon) => <- iy. move => c cp ic. by rewrite (least_rem_p4 iy cp) (least_rem_p5 iy). have nyi: ~ indecomposable y. move: (osum_Meqlt rz oon); rewrite (osum0r oon) - yv2 => la. by move =>[_ h];move: (h _ _ la lry); rewrite - yv2; case. have H c :is_rem_of y c -> indecomposable c -> c = least_rem r. move => [cp [a oa yv1]] ic; move: (proj32_1 cp) => oc. case: (oleT_el oon oa) => coa. move:(odiff_pr coa); set a' := _ -o _; move => [oa' eq2]. have eq3: oopow n +o (a' +o c) = oopow n +o r. by rewrite (osumA oon oa' oc) - eq2 - yv2 - yv1. move:(osum2_simpl (OS_sum2 oa' oc) or oon eq3) => eq4. have rc: is_rem_of r c by split => //; exists a'. have: inc r y by apply/oltP. move/yleast => pr; exact: (pr rz c rc ic). case: nyi. move:(ord_negl_opow coa on) => na. move:(ord_negl_sum oa oon or na). rewrite - yv2 yv1 => /(ord_neg_sum4 oa (proj32_1 cp)). by rewrite/ord_negl - yv1 => ->. move => c ca cb; rewrite (H c ca cb). by rewrite (H _ (least_rem_p1 yp) (least_rem_p3 yp)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)