proposition: Lemma totient_count_coprime n : totient n = \sum_(0 <= d < n) coprime n d.
proof: Proof. elim/ltn_ind: n => // n IHn. case: (leqP n 1) => [|lt1n]; first by rewrite unlock; case: (n) => [|[]]. pose p := pdiv n; have p_pr: prime p by apply: pdiv_prime. have p1 := prime_gt1 p_pr; have p0 := ltnW p1. pose np := n`_p; pose np' := n`_p^'. have co_npp': coprime np np' by rewrite coprime_partC. have [n0 np0 np'0]: [/\ n > 0, np > 0 & np' > 0] by rewrite ltnW ?part_gt0. have def_n: n = np * np' by rewrite partnC. have lnp0: 0 < logn p n by rewrite lognE p_pr n0 pdiv_dvd. pose in_mod k (k0 : k > 0) d := Ordinal (ltn_pmod d k0). rewrite {1}def_n totient_coprime // {IHn}(IHn np') ?big_mkord; last first. by rewrite def_n ltn_Pmull // /np p_part -(expn0 p) ltn_exp2l. have ->: totient np = #|[pred d : 'I_np | coprime np d]|. rewrite [np in LHS]p_part totient_pfactor //=; set q := p ^ _. apply: (@addnI (1 * q)); rewrite -mulnDl [1 + _]prednK // mul1n. have def_np: np = p * q by rewrite -expnS prednK // -p_part. pose mulp := [fun d : 'I_q => in_mod _ np0 (p * d)]. rewrite -def_np -{1}[np]card_ord -(cardC [in codom mulp]). rewrite card_in_image => [|[d1 ltd1] [d2 ltd2] /= _ _ []]; last first. move/eqP; rewrite def_np -!muln_modr ?modn_small //. by rewrite eqn_pmul2l // => eq_op12; apply/eqP. rewrite card_ord; congr (q + _); apply: eq_card => d /=. rewrite !inE [np in coprime np _]p_part coprime_pexpl ?prime_coprime //. congr (~~ _); apply/codomP/idP=> [[d' -> /=] | /dvdnP[r def_d]]. by rewrite def_np -muln_modr // dvdn_mulr. do [rewrite mulnC; case: d => d ltd /=] in def_d *. have ltr: r < q by rewrite -(ltn_pmul2l p0) -def_np -def_d. by exists (Ordinal ltr); apply: val_inj; rewrite /= -def_d modn_small. pose h (d : 'I_n) := (in_mod _ np0 d, in_mod _ np'0 d). pose h' (d : 'I_np * 'I_np') := in_mod _ n0 (chinese np np' d.1 d.2). rewrite -!big_mkcond -sum_nat_const pair_big (reindex_onto h h') => [|[d d'] _]. apply: eq_bigl => [[d ltd] /=]; rewrite !inE -val_eqE /= andbC !coprime_modr. by rewrite def_n -chinese_mod // -coprimeMl -def_n modn_small ?eqxx. apply/eqP; rewrite /eq_op /= /eq_op /= !modn_dvdm ?dvdn_part //. by rewrite chinese_modl // chinese_modr // !modn_small ?eqxx ?ltn_ord. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(fintype div bigop)