proposition: Lemma ffactn1 n : natp n -> n ^_c \1c = n.
proof: Proof. move => nN. rewrite - succ_zero (ffactnSr _ NS0) ffactn0 (cdiff_n0 nN) cprod1l; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)