proposition: Lemma fusc_totient b: 0 < b -> \sum_(i< 2^ b.-1) (b== fusc (i.*2.+1)) = totient b.
proof: Proof. set m := 2^ b.-1 => bp. move:(prednK bp); set b' := b.-1; move => sa. have Ha: forall i, fusc i < fusc (i.*2.+1). by move => i; rewrite fusc_odd ltn_paddr // fusc_gt0. pose f (i: 'I_m) := inord (fusc i): 'I_(b'.+1). set D := [pred i:'I_m |b == fusc i.*2.+1]. have: {in D &, injective f}. move => u v; rewrite ! inE => /eqP ea /eqP eb sb. have hu: fusc u < b'.+1 by rewrite sa ea; apply: Ha. have hv: fusc v < b'.+1 by rewrite sa eb; apply: Ha. apply:ord_inj;apply/eqP; rewrite - eqn_double. apply/eqP/fuscp_injective; last by rewrite - ea - eb. by rewrite !fusc_even - (inordK hu) - (inordK hv) -/(f u) -/(f v) sb. move/card_in_imset; rewrite - (sum1_card D) big_mkcond /= => <-. have <-: #|[set i:'I_(b'.+1) | coprime b i]| = totient b. rewrite totient_count_coprime big_mkord - sum1_card big_mkcond sa //=. by apply: congr_big => // i _ /=; rewrite inE. apply: eq_card => a; rewrite inE; apply/imsetP/idP. move => [i]; rewrite inE => /eqP ea eb. have hu: fusc i < b'.+1 by rewrite sa ea; apply: Ha. by rewrite ea eb /f (inordK hu) - (fusc_even i) coprime_sym fusc_coprime. move => ce;move:(ltn_ord a); rewrite {2} sa => lab. move: (subnK (ltnW lab)); set c := _ - _; rewrite addnC => ea. have cap: coprime a c by move: ce; rewrite - ea /coprime gcdnC gcdnDl. move:lab; rewrite - subn_gt0; rewrite -/c => cp. rewrite - (prednK cp) in cap. move: (fusc_pair_surj cap) => [n [ha hb]]. have bn: b = fusc (n.*2.+1) by rewrite -ea ha - (prednK cp) hb fusc_odd. have lnm: n < m. rewrite /m bn -ltn_double -expn2S prednK ?fusc_gt0 //. apply: fusc_lower_bound. exists (Ordinal lnm); rewrite ? inE ? bn // /f - ha inord_val //. 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)