proposition: Lemma nds_type_exists_bd n k: natp n -> \0c <c k -> k <=c n -> exists X, nds_ax X n /\ nds_type X n k.
proof: Proof. move => nN kp lkn. have kz := (nesym (proj2 kp)). pose X i := Yo (i <c k) \1o omega0. have ha: nds_ax X n by move => t _; rewrite /X; Ytac h; fprops. have hb: opos_below X n. move => i _; rewrite /X; Ytac h; [apply: olt_01| apply: olt_0omega]. exists X; split => //; split => //. move: odegree_one odegree_omega => dg1 dgo. exists \0o; split; [ exact: OS0 | by move => i /ha/OS_degree /ole0x | ]. set E := Zo _ _. move:(NS_le_nat lkn nN) => kN. rewrite -(card_nat kN); congr cardinal. set_extens t. move => /Zo_P [ /(NltP nN) lth]; rewrite /X; Ytac h1. by move => _; apply/(NltP kN). by rewrite dgo => ba; case: card1_nz. move => /(NltP kN) ltl;apply: Zo_i. apply /(NltP nN); exact:(clt_leT ltl lkn). by rewrite /X; Ytac0; rewrite dg1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)