proposition: Lemma NS_ffact n m: natp n -> natp m -> natp (n ^_c m).
proof: Proof. move => nN; move: m; apply: Nat_induction. rewrite ffactn0; apply: NS1. move => m mN Hr; rewrite (ffactnSr _ mN); apply: (NS_prod Hr); fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)