proposition: Lemma nat_to_B_binom m n: nat_to_B 'C(m,n) = binom (nat_to_B m) (nat_to_B n).
proof: Proof. have H:= nat_to_B_Nat. move:m n; elim. case => //; first by rewrite binom0 -? succ_zero //; fprops. by move => m; rewrite bin0n /= binom0Sm. move => n Hr [| m]. rewrite bin0 binom0 - ? succ_zero //; apply: nat_to_B_Nat. rewrite binS nat_to_B_sum Hr Hr - !nat_to_B_succ - binomSnSm //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)