proposition: Lemma divn_count_dvd d n : n %/ d = \sum_(1 <= i < n.+1) (d %| i).
proof: Proof. have [-> | d_gt0] := posnP d; first by rewrite big_add1 divn0 big1. apply: (@addnI (d %| 0)); rewrite -(@big_ltn _ 0 _ 0 _ (dvdn d)) // big_mkord. rewrite (partition_big (fun i : 'I_n.+1 => inord (i %/ d)) 'I_(n %/ d).+1) //=. rewrite dvdn0 add1n -[_.+1 in LHS]card_ord -sum1_card. apply: eq_bigr => [[q ?] _]. rewrite (bigD1 (inord (q * d))) /eq_op /= !inordK ?ltnS -?leq_divRL ?mulnK //. rewrite dvdn_mull ?big1 // => [[i /= ?] /andP[/eqP <- /negPf]]. by rewrite eq_sym dvdn_eq inordK ?ltnS ?leq_div2r // => ->. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(fintype div bigop)