proposition: Lemma fusc_totient_prime b (H := fun b => \sum_(2^(b.-1) <= i< 2^ b) (b== fusc i) = b .-1) : (prime b -> H b) /\ (0 < b -> H b -> prime b).
proof: Proof. split. move => h. have bp:= (prime_gt0 h). move: (leqnn b); rewrite - {2} (prednK bp) => h2. move:(fusc_totient2 bp h2); rewrite (prednK bp). by rewrite (totient_pfactor h (ltn0Sn 0)) muln1. move => bp; move: (leqnn b); rewrite - {2} (prednK bp) totient_prime bp => h2. by move:(fusc_totient2 bp h2); rewrite /H (prednK bp) => -> ->; rewrite eqxx. 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)