proposition: Lemma binzE_ffact (F : numFieldType) (m n : nat) : (binomialz (Posz n) (Posz m))%:~R = (Posz (n ^_ m))%:~R / (Posz m`!)%:~R :> F.
proof: Proof. apply/eqP; rewrite binz_nat_nat -bin_ffact !PoszM !rmorphM mulfK //=. by rewrite pnatr_eq0 lt0n_neq0 ?fact_gt0. Qed.
imports: mathcomp(all_ssreflect all_algebra) tactics