proposition: Lemma ord_factor10 p n: ofact_list_succ p (csucc n) -> natp n -> ~ (natp (p \0c)) -> exists ec m, [/\ natp m, CNFp_ax ec (csucc m), oprodf p (csucc n) = CNFpv ec (csucc m) & [/\ ec (csucc m) = J \0o \1o, let p' := p \o csucc in Q(ec \0c) = oprodf p' (first_non_int p' n) & P(ec \0c) = odegree (p \0c) ]].
proof: Proof. move => ha hb hc. move:(ord_factor9 ha hb hc) => [ec [m [mN r2 r3 r4 r5]]]. pose ec1 i := Yo (i = csucc m) (J \0o \1c) (ec i). have smN := NS_succ mN. have ec1mv: ec1 (csucc m) = J \0o \1c by rewrite /ec1; Ytac0. have xx: ec1 \0c = ec \0c by rewrite /ec1 (Y_false (nesym (@succ_nz m))). rewrite - xx in r4. have e10v: P(ec1 \0c) = odegree (p \0c). by ue. have ax1: CNFp_ax ec1 (csucc m). rewrite /ec1;split; last by Ytac0; split; aww; apply: PN1. by move => i lim; rewrite /ec1 (Y_false (proj2 lim)); apply: r2. have v1: oprodf p (csucc n) = CNFpv ec1 (csucc m). rewrite /CNFpv r3 /ec1; Ytac0; aw; rewrite oopow0 (oprod1r OS1). set u := CNFpv1 _ _; set v := CNFpv1 _ _. have -> : v = u. by apply:(oprodf_exten smN) => i [_ lin]; rewrite/cantor_pmon; Ytac0. have ou : ordinalp u by apply:(OS_CNFp1 r2 smN). by rewrite (oprod1l ou). by exists ec1, m; split. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)