proposition: Lemma combinaisonE n0 m0 : (m0 <= n0)%nat -> C n0 m0 = 'C(n0, m0)%:R.
proof: Proof. move=> ?. rewrite /C. apply (@eqR_mul2r (INR (fact m0) * INR (fact (n0 - m0)%coq_nat))). move/eqP; rewrite mulR_eq0' !INR_eq0' => /orP[|] /eqP; exact/fact_neq_0. set tmp := INR (fact m0) * _. rewrite -mulRA mulVR ?mulR1; last first. by rewrite /tmp mulR_neq0' !INR_eq0' !factE -!lt0n !fact_gt0. by rewrite /tmp -!natRM !factE !minusE bin_fact. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) Reals mathcomp(lra) mathcomp(Rstruct)