proposition: Lemma nds_f2: nds_F \2c = \2c.
proof: Proof. apply: cleA. by move: (proj42 (nds_f_def NS2)); rewrite factorial2. by move: (nds_sd1 NS1); rewrite (cpowx1 CS2) succ_one. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)