proposition: Lemma nds_type_nor_ex X n k: natp n -> \0c <c k -> k <=c n -> nds_type X n k -> exists Y e, [/\ nds_type_nor Y n k e & nds_card Y n = nds_card X n].
proof: Proof. move => nN knz lekn [ha [m [om h1]]]. set E := Zo _ _ => ce. have ax:nds_ax X n by move => i /ha/proj32_1. have sk: sub k n by case: lekn. have kN:=(NS_le_nat lekn nN). have sE: sub E n by apply: Zo_S. case: (nth_elt_dbl_prop2 nN sE); set f := Lf _ _ _; move => fp; rewrite ce. move: (nds_card_perm_inv nN ax fp); set Y:= fun i =>X (Vf f i) => yv fv. rewrite yv. exists Y,m; split; last reflexivity. move:fp => /Zo_P [/functionsP [ff sf tf] bf] . have sisf: sub k (source f) by rewrite sf. move: (cardinal_image sisf (proj1 bf));rewrite- fv (card_nat kN) => ck. have pa i: i <c n -> \0o <o (Y i). move => /(NltP nN) ii; apply: ha; apply/(NltP nN); Wtac. have pb i: i <c n -> m <=o odegree (Y i). move => /(NltP nN) ii; apply: h1;apply/(NltP nN); Wtac. have pc: forall i, i <c k -> odegree (Y i) = m. move => i /(NltP kN) ik. have/Zo_hi //: inc (Vf f i) E by rewrite fv; apply/(Vf_image_P ff sisf); ex_tac. have pd: (Zo n (fun i => odegree (Y i) = m)) = k. set_extens t. move => /Zo_P [ta tb]. have: inc (Vf f t) E by apply:Zo_i; [Wtac | apply: tb ]. rewrite fv => /(Vf_image_P ff sisf) [u usf]. move: ta (sk _ usf); rewrite - sf => hb hc hd. by rewrite(proj2(proj1 bf) _ _ hb hc hd). move => ta; apply /Zo_P;split; first by apply: sk. by apply: pc; apply /(NltP kN). have pe i: k <=c i -> i <c n -> m <o odegree (Y i). move => ki kin; split; [ by apply: pb | move => sa ]. have: inc i k. by rewrite - pd; apply /Zo_P; split; [by apply/(NltP nN) | done]. by move/(NltP kN) => /(cleNgt ki). have pf:nds_type Y n k. split;[ exact| exists m]; rewrite pd (card_nat kN); split; exact. split; exact. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)