proposition: Lemma nat_to_B_fact n: nat_to_B (n`!) = factorial (nat_to_B n).
proof: Proof. elim: n; first by rewrite factorial0 fact0 - succ_zero //. move=> n Hr; rewrite factS nat_to_B_prod Hr - nat_to_B_succ cprodC. rewrite factorial_succ //; apply: nat_to_B_Nat. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)