proposition: Lemma nds_card_same_deg_bd e X n: natp n -> \0c <c n -> (opos_below X n) -> (forall i, i <c n -> odegree (X i) = e) -> nds_card X n <=c n.
proof: Proof. move => nN nz pa pb. pose c i := the_cnf_lc (X i). pose r i := the_cnf_rem (X i). have pc i: i<c n -> [/\ \0o <o c i, c i <o omega0, (r i) <o oopow e & X i = oopow e *o (c i) +o (r i)]. move => lein; move: (pa _ lein) (pb _ lein) => sa sb. by move: (the_cnf_split sa); rewrite sb. have oe: ordinalp e. rewrite -(pb _ nz); exact: (OS_degree (proj32_1 (pa _ nz))). set s1:= oopow e *o (osumf c n). have os1: ordinalp s1. apply: (OS_prod2 (OS_oopow oe) (OS_osumf nN _)) => i lin. by move:(pc _ lin) => [ /proj32_1 h _ _ _]. set E := (permutations n). set F1 := (fun_image E (nds_sc X n)). set F2 := (fun_image E (fun f => r (Vf f \0c))). have pe i: i<c n -> c i <o omega0 by move => /pc[]. have pd i: i<c n -> \0o <o c i /\ r i <o oopow e by move => /pc[]. have pf: forall f, inc f E -> nds_sc X n f = s1 +o (r (Vf f \0c)). move => f fp; rewrite - (nds_same_deg_s_perm nN nz oe pd pe fp). by apply:(nds_sc_exten nN _ fp) => i /pc []. have pg: forall z, inc z E -> inc (Vf z \0c) n. move => z /Zo_P [] /functionsP [fz sz tz] bz; Wtac. by rewrite sz; apply/(NltP nN). have osF: ordinal_set F2. by move=> s /funI_P [z /pg /(NltP nN) /pc [_ _ /proj31_1 h _] ->]. suff: nds_card X n = cardinal (fun_image n r). move ->; rewrite -{2} (card_nat nN); apply:fun_image_smaller. symmetry. apply/card_eqP. exists (Lf (fun z => s1 +o z) F2 F1); split. * apply:lf_bijective. + by move => s /funI_P [z ze -> ]; apply /funI_P; ex_tac; rewrite (pf _ ze). + by move => u v /osF ou /osF ov /(osum2_simpl ou ov os1). + move => s /funI_P [z ze -> ]; rewrite (pf _ ze). exists (r (Vf z \0c)) => //;apply/funI_P; ex_tac. * rewrite lf_source;set_extens t. move => /funI_P [z /pg ze -> ]; apply /funI_P; ex_tac. move => /funI_P [i /(NltP nN) iI ->]; apply /funI_P. move: (permutation_exists1 nN iI) => [f fe <-]; ex_tac. * by aw. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)