proposition: Lemma fusc_totient2 n b: 0 < b -> b <= n.+1 -> \sum_(2^n <= i< 2^(n.+1)) (b== fusc i) = totient b.
proof: Proof. set m := 2^ n.+1. move => sa sb; rewrite -(fusc_totient sa). move:(prednK sa); set b' := b.-1; move => sac. have sc: 2 ^ b' <= 2 ^ n by rewrite leq_exp2l // -ltnS sac. pose g i := (i.*2.+1) * 2 ^(n.+1 - log2 (i.*2.+1)). have Hb: forall i, b = fusc i.*2.+1 -> b = fusc (g i). by move => i ->; rewrite /g mulnC fusc_kpow2n. have Ha: forall i, i < 2 ^ b' -> 2^n <= g i < m. move => i ha;move/andP:(log2_bnd i.*2) => [hb hc]. set j := i.*2.+1. have hb': 2 ^ log2 j <= j.*2 by rewrite log2S_k expn2S leq_double. have hd: log2 j <= n.+1. apply: leq_trans sb; rewrite - ltnS -(ltn_exp2l _ _ (ltnSn 1)). apply: (leq_ltn_trans hb'); rewrite expn2S ltn_double /j - sac. by rewrite - doubleS expn2S leq_double. rewrite /g /m - leq_double - expn2S - {1 4} (subnKC hd) expnD ltn_mul2r. rewrite expn_gt0 hc /= - mul2n mulnA mul2n leq_pmul2r ? hb' ? expn_gt0 //. pose M := 2^b'. have mp: 0 < m by rewrite /m expn_gt0. move:(prednK mp); set m' := m.-1 => mpp. pose f (i: 'I_M) := inord (g i): 'I_m'.+1. set D := [pred i:'I_M |b == fusc i.*2.+1]. have Hc: forall u: 'I_M, (@nat_of_ord m'.+1 (inord (g u))) = g u. by move => u; move /andP: (Ha _ (ltn_ord u)) => [_]; rewrite -mpp => /inordK. have: {in D &, injective f}. move => u v; rewrite ! inE /f => /eqP ea /eqP eb ec; apply: ord_inj. move: (f_equal (@nat_of_ord m'.+1) ec). by rewrite (Hc u) (Hc v) /g; move/elogn2_unique. move/card_in_imset; rewrite - (sum1_card D) big_mkcond /= => <-. set x := LHS. have: x = #|[set i:'I_m'.+1 | (2^n <= i) && (b == fusc i) ]|. rewrite - sum1dep_card big_mkcondr /=. rewrite - (big_mkord _ (fun i => if (b == fusc i) then 1 else 0)). have qa: 0 <= 2^n by []. have qb: 2^n <= m'.+1 by rewrite mpp /m expn2S double_le1. rewrite (big_cat_nat _ _ _ qa qb) /= big1_seq. by rewrite add0n big_mkcond /= /x mpp; apply: eq_big_nat => i /andP[->]. by move => i; rewrite mem_iota add0n subn0 ltnNge => /and3P [->] //. move => ->; clear x; apply: eq_card => a; rewrite inE; apply/idP/imsetP. move => /andP [pa pb]; rewrite /f. case: (posnP a) => az; first by move: sa; rewrite (eqP pb) az fusc0. case: (elogn2P a.-1) => e q; rewrite (prednK az) => aq. have fq: fusc (q.*2.+1) = b by rewrite (eqP pb) aq fusc_kpow2n. move: (fusc_lower_bound q); rewrite fq - sac expn2S ltn_double => qm. have: 2^n <= a < 2^n.+1 by rewrite pa -/m - mpp (ltn_ord a). move/log2_pr; rewrite aq mulnC log2_mul_exp // => aa. exists (Ordinal qm); first by rewrite inE fq. by apply:ord_inj;rewrite Hc /= /g - aa addnK mulnC. move => [x]; rewrite inE /f => qa qb. move:(Ha _ (ltn_ord x)) => /andP[ra rb]; rewrite qb inordK ? mpp // ra /=. by apply /eqP /Hb /eqP. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq choice fintype order bigop ssralg) mathcomp(div ssrnum ssrint rat prime path binomial) mathcomp(tuple finset) gaia(fibm)