proposition: Lemma cnfnat_sum_rem n a x: ordinalp n -> a <o omega0 -> x <o oopow n -> (oopow n *o a +o x) = (oopow n *o a +#o x).
proof: Proof. move => on lao lxo. have ox := proj31_1 lxo. have oa := proj31_1 lao. have ooa:= (OS_prod2 (OS_oopow on) oa). case: (ozero_dichot oa) => az. by rewrite az oprod0r (osum0l ox) natural_sumC (natural_sum0 ox). have pa: posnatp a by apply/ posnat_ordinalp. case: (ozero_dichot ox) => xp. by rewrite xp (osum0r ooa) (natural_sum0 ooa). move: (cnf_one_term on pa); set A := Lg _ _; move => [cA _ eqA1 eqA2]. move: (the_cnf_p0_nz xp) => [qa qb]. have qc: \0c <c domain A by rewrite /A Lgd; fprops. have i01: inc \0c \1c by apply: set1_1. have qd1: cnf_degree (the_cnf x) <o n. by move:(the_cnf_p6 on xp lxo); rewrite /odegree (Y_false (nesym (proj2 xp))). have qd: cnf_degree (the_cnf x) <o oexp A \0c. by rewrite /A/oexp LgV//; aw. have qe: (\0c = \0c \/ oexp A (cpred \0c) <o cnf_degree (the_cnf x)) by left. move: (CNF_sum_pr1 cA qa qc qd qe); rewrite eqA2 qb; move ->. have ->: (cnf_ns A \0c) = A. rewrite /cnf_ns/cnf_s /A Lgd (cdiff_n0 NS1); apply: Lg_exten. move => i i1 /=; rewrite LgV//(csum0r) //; move/set1_P: i1 => ->; fprops. have qa1 := proj1 qa. have qf1 i:i <c domain (the_cnf x) -> oexp (the_cnf x) i <=o cnf_degree (the_cnf x). move: (cnf_size_nz qa) => [ra rb] idx. have nN:= proj42 qa1. apply: (CNF_exponents_M nN (proj1(proj44 qa1))). apply/(cltSleP ra); ue. by rewrite rb; apply/cltS. have qf: cnfp (cnf_nm (the_cnf x) A). apply: (cnfp_cnf_nm qa1 cA) => i j; rewrite /A Lgd;move => idx /clt1 ->. rewrite {2}/oexp LgV//; aw; apply: (ole_ltT (qf1 _ idx) qd1). congr cnf_val. rewrite eqA1; apply: (cnf_nat_sum_p3 cA (proj1 qa) qf) => e. rewrite Vr_monomial /Vr (cnfp_cnf_nm_range qa1 cA) /A Lg_range funI_set1. move: (cnf_range_fgraph (proj1 qa)); set R := range _ => fgr. have qg: ~ inc n (domain R). move/funI_P => [z /(range_gP (proj41 qa1)) [i idx ->]] => nv. have ii: i <c (domain (the_cnf x)) by apply/(NltP (proj42 qa1)). by case:(oltNge qd1); rewrite nv; exact: (qf1 i ii). case: (equal_or_not e n) => en; Ytac0. by rewrite en (setU1_V_out _ fgr qg) (Vg_out_of_range qg) (Nsum0r (proj1 pa)). case: (inc_or_not e (domain R)) => edr. have qh: (natp (Vg R e)). apply: (NS_Vr _ qa1). by rewrite (setU1_V_in _ fgr qg edr) (Nsum0l qh). have qh: ~ inc e (domain (R +s1 J n a)) by rewrite domain_setU1 => /setU1_P; case. by rewrite (Vg_out_of_range edr) (Vg_out_of_range qh) (csum0r CS0). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)