proposition: Corollary dvd_nbin_iter_lcmn (i j : nat) (n : nat) : 1 <= j -> j <= i -> i <= n -> j * 'C(i, j) %| l n.
proof: Proof. move=> le0j leji lein. apply/dvdn_partP => [|p hp]; first by rewrite muln_gt0 bin_gt0 le0j. apply: dvdn_trans ( iter_lcmn_leq_div lein); move: hp. rewrite mem_primes; case/and3P=> pp hpos hdvd. rewrite p_part pfactor_dvdn //. exact: bin_valp. Qed.
imports: mathcomp(all_ssreflect all_algebra)