proposition: Lemma NS_binom n m: natp n -> natp m -> natp (binom n m).
proof: Proof. move=> nN; move: n nN m; apply: Nat_induction. apply: Nat_induction; first by rewrite binom00=>//; fprops. move => n nN _; rewrite binom0Sm; fprops. move => n nN hrec; apply: Nat_induction; first by rewrite binomSn0; fprops. move => p pN bN; rewrite binomSnSm; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)