proposition: Lemma nds_sd2 n: natp n -> \2c <c n -> n <c (nds_F n).
proof: Proof. move => nN ngt2. have nnz:= nesym (proj2(clt_ltT clt_02 ngt2)). move:(cpred_pr nN nnz) => [n1N sa]. have npz: cpred n <> \0c. move => h; move: sa (proj1 ngt2). by rewrite h succ_zero => -> /(cltNge clt_12). move:(cpred_pr n1N npz) => [n2N sb]. have pN:= NS_pow NS2 n2N. have ha : \2c <=c \2c ^c cpred (cpred n). apply:(cpow_Mle1 CS2) => mz. by case:(proj2 ngt2); rewrite sa sb mz succ_zero succ_one. have hb: csucc (cpred n) <c \2c ^c cpred n. rewrite sb (cpow_succ _ n2N) cprodC - csum_nn. rewrite (Nsucc_rw (NS_succ n2N)) (Nsucc_rw n2N) - csumA csum_11 csumC. exact:(csum_Mlelt pN ha (cantor (CS_nat n2N))). rewrite sa; exact: (clt_leT hb (nds_sd1 n1N)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)