proposition: Lemma binzE (F : numFieldType) (m n : nat) : (m <= n)%N -> (binomialz (Posz n) (Posz m))%:~R = (Posz n`!)%:~R / ((Posz m`!)%:~R * (Posz (n - m)`!)%:~R) :> F.
proof: Proof. move=> hmn; rewrite binz_nat_nat; apply/eqP. rewrite -(bin_fact hmn) !PoszM !rmorphM mulfK //=. by apply/mulf_neq0; rewrite pnatr_eq0 lt0n_neq0 ?fact_gt0. Qed.
imports: mathcomp(all_ssreflect all_algebra) tactics