proposition: Lemma nds_sd1 n: natp n -> \2c ^c n <=c nds_F (csucc n).
proof: Proof. move => nN. move: (nds_card_different_deg nN) => [ra rb]. move: (nds_f_def (NS_succ nN)) => [_ _ _ rc]. by move: (rc _ ra); rewrite rb. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)