proposition: Lemma nds_tn_value n: natp n -> nds_tn_sup n = ndsC n.
proof: Proof. move => nN. case: (czero_dichot (CS_nat nN)) => np. by rewrite np nds_tn_zero /ndsC cprodC cprod0r succ_zero. move: (nds_tn_def nN) => [_ _ [X hx eq1] hu]. apply: cleA; first by rewrite - eq1; exact:(nds_tn_max nN np hx). rewrite - (nds_tn_ex_val nN); apply: (hu _ (nds_tn_ex_ax nN)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)